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):
Axiomatically defined operators are not supported without additional annotations.
An example project with theories: media:theories2.zip
The project contains the following theories:
The operators are annotated such that ProB uses an extra implementation.
The mkinat operator is annotated such that ProB uses an explicit implementation.
The operator is annotated such that ProB uses an extra implementation.
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 |