Line 39: | Line 39: | ||

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

'''Please note:''' The use of these tags is | '''Please note:''' The use of these tags is 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. | 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. |

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 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 |