Line 12: | Line 12: | ||

An example project with theories: [[media:theories2.zip]] | An example project with theories: [[media:theories2.zip]] | ||

' | The project contains the following theories: | ||

; SUMandPRODUCT | |||

: Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value. | |||

The operators are annotated such that ProB uses an extra implementation. | |||

; Seq | |||

: The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB. | |||

; Real (unsupported) | |||

: A theory of real numbers, currently unsupported by ProB. | |||

; Natural | |||

: A theory of inductive naturals (defined by a constant zero and a successor function). | |||

The mkinat operator is annotated such that ProB uses an explicit implementation. | |||

; List | |||

: A theory of lists that are either empty or have a head and a tail | |||

; FixPoint (not really supported) | |||

: The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them. | |||

; closure | |||

: The operator for transitive closures is supported by ProB. | |||

The operator is annotated such that ProB uses an extra implementation. | |||

; Card (contains no operators or data types) | |||

: Contains theorem about set cardinalities. | |||

; BoolOps | |||

: Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB. | |||

; BinaryTree | |||

: Binary Trees are supported by ProB. | |||

== Tagging operators == | == Tagging operators == |

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):

- recursive datatypes (e.g. the List datatype)
- operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
- special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

An example project with theories: media:theories2.zip

The project contains the following theories:

- SUMandPRODUCT
- Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.

The operators are annotated such that ProB uses an extra implementation.

- Seq
- The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
- Real (unsupported)
- A theory of real numbers, currently unsupported by ProB.
- Natural
- A theory of inductive naturals (defined by a constant zero and a successor function).

The mkinat operator is annotated such that ProB uses an explicit implementation.

- List
- A theory of lists that are either empty or have a head and a tail
- FixPoint (not really supported)
- The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
- closure
- The operator for transitive closures is supported by ProB.

The operator is annotated such that ProB uses an extra implementation.

- Card (contains no operators or data types)
- Contains theorem about set cardinalities.
- BoolOps
- Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
- BinaryTree
- Binary Trees are supported by ProB.

**Please note:** The use of these tags is usually for experts only. Normally such annotations are delivered with a theory. If you think ProB should provide specific support for a theory, please contact us.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file (**P**roB **T**heory **M**apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form

operatorNameinternal {Tag}

where **Name** is the name of the operator in the theory and **Tag** is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):

Tag | Description | Expected type | Return type |
---|---|---|---|

closure1 | the transitive closure | POW(T**T) | POW(T**T) |

SIGMA | the sum of a set | POW(T**INT) | INT |

PI | the product of a set | POW(T**INT) | INT |

mu | returns the element of a singleton set | POW(T) | T |

choose | returns (deterministically) one element of a non-emtpy set | POW(T) | T |

mkinat(zero,succ) | returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) | INT | Inductive Nat |