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

Axiomatically defined operators are not supported without additional annotations.

Download Theories

An example project with theories: media:theories2.zip

TODO: A description of the supported parts.

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.

The use of these tags is usually for experts only. In the theory file below, some of the theories are annotated.

Currently are the following tags supported:

TODO: to be continued...