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

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