(Created page with '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…') |
|||

Line 15: | Line 15: | ||

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

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

Line 23: | Line 25: | ||

where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name. | 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): | |||

Currently are the following tags supported: | |||

{| class="wikitable" | {| class="wikitable" | ||

! Tag || Description | ! Tag || Description || Expected type || Return type | ||

|- | |- | ||

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

|- | |- | ||

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

|- | |- | ||

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

|- | |- | ||

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

|- | |- | ||

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

|- | |- | ||

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

|} | |} | ||

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

**TODO**: A description of the supported parts.

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