Event-B Theories

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 like transitive closure (see below)

Axiomatically defined operators are not supported without additional annotations.

Download Theories

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 closure is supported by ProB.; The operator is annotated such that ProB uses the classical B 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

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

As of version 1.12 (mid-september 2022) ProB also transparently accepts POW(INT) as type for SIGMA and PI. It now also accepts many of its external functions as tag names, such as the the functions from LibraryStrings.def or LibraryReals.def. For example, here we map the operator plus to ProB's external function RADD for adding two reals:

operator "plus" internal {RADD}

If you set the preference AUTO_DETECT_THEORY_MAPPING to TRUE then ProB will work with several standard Rodin theories even without a .ptm file in the workspace.

As of version 1.13 (November 2023) ProB also accepts literals as well as formulas between dollars in the .ptm files. For example, here the operator Rone is defined by the literal 1.0 and the operator RRealPlus by an expression (a set comprehension of the positive reals annotated with the symbolic pragma):

operator "Rone" internal {1.0}
operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$}

Error Messages

In case the .ptm file is missing, you will get an error message such as the following one:

Axiomatic defined operator "SUM" not recognized.

Examples

For reference, here are the contents of some of the .ptm files. In case of an error message, you can copy these files into your Theory Projects (e.g., using Drag & Drop) and then refresh (F5). After that animation with ProB should work.

SUMandPRODUCT.ptm

operator "SUM" internal {SIGMA}
operator "PRODUCT" internal {PI}

closure.ptm

operator "cls" internal {closure1}

Natural.ptm

operator "mk_iNAT" internal {mkinat}

Here are the contents for a Reals theory by Guillaume Dupont:

operator "RReal" internal {REAL}
operator "Rone" internal {1.0}
operator "Rzero" internal {zero}
operator "Rtwo" internal {two}
operator "plus" internal {RADD}
operator "times" internal {RMUL}
operator "minus" internal {RSUB}
operator "lt" internal {RLT}
operator "leq" internal {RLEQ}
operator "gt" internal {RGT}
operator "geq" internal {RGEQ}
operator "uminus" internal {RSUB}
operator "inverse" internal {RINV}
operator "divide" internal {RDIV}
operator "abs" internal {RABS}
operator "sqrt" internal {RSQRT}
operator "Rmax" internal {RMAXIMUM}
operator "Rmin" internal {RMINIMUM}
operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$}
operator "RRealMinus" internal {$/*@symbolic*/ {x|x:REAL & x<= 0.0}$}
operator "RRealStar" internal {$/*@symbolic*/ {x|x:REAL & x /= 0.0}$}
operator "RRealPlusStar" internal {$/*@symbolic*/ {x|x:REAL & x> 0.0}$}
operator "RRealMinusStar" internal {$/*@symbolic*/ {x|x:REAL & x< 0.0}$}