Event-B Theories: Difference between revisions

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

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):

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}$}