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 |