External Functions

As of version 1.3.5-beta7 ProB can make use of externally defined functions. These functions must currently be written in Prolog (in principle C, Java, Tcl or even other languages can be used via the SICStus Prolog external function interfaces). These functions can be used to write expression</m>, predicates, or substitutions.

Currently, these external functions are linked to classical B machines using DEFINITIONS as follows:

one definition, which defines the function as it is seen by tools other than ProB (e.g., Atelier-B)

one definition declaring the type of the function

Prolog code which gets called by ProB in place of the right-hand-side of the first definition
Usually, it is also a good idea to encapsulate the external function inside a CONSTANT which is defined as a lambda abstraction with as body simply the call to the first DEFINITION. This allows one to compute the domain, range, ... of the function.
In a first instance we have predefined a series of external functions and grouped them in various library machines and definition files:
LibraryMath.mch

LibraryStrings.mch