(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):
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 (ProB Theory Mapping). The file must have the same name as the theory.
For each annotated operator, the file contains a line of the form
operator Name internal {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 |