(Created page with ' 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 languag…') |
No edit summary |
||
| Line 1: | Line 1: | ||
[[Category:User Manual]] | |||
[[Category: Advanced Feature]] | |||
As of version 1.3.5-beta7 ProB can make use of externally defined functions. | As of version 1.3.5-beta7 ProB can make use of externally defined functions. | ||
| Line 5: | Line 7: | ||
Currently, these external functions are linked to classical B machines using DEFINITIONS as follows: | 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, which defines the function as it is seen by tools other than ProB (e.g., Atelier-B). E.g., if we want to declare an external function named <tt>COS</tt>, this would be <tt>COS(x) == cos(x)</tt>. | ||
* one definition declaring the type of the function | * one definition declaring the type of the function. For <tt>COS</tt> this would be <tt>EXTERNAL_FUNCTION_COS == INTEGER --> INTEGER</tt>. | ||
* Prolog code which gets called by ProB in place of the right-hand-side of the first definition | * 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. | 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. For <tt>COS</tt> this would be <tt>cos = %x.(x:NATURAL|COS(x))</tt>. Observe that for Atelier-B this is a tautology. | ||
For ProB, the use of such a constant allows one to have a real B function representing the external function, for which we can compute the domain, range, etc. | |||
In a first instance we have predefined a series of external functions and grouped them in various library machines and definition files: | In a first instance we have predefined a series of external functions and grouped them in various library machines and definition files: | ||
* <tt>LibraryMath.mch</tt> | * <tt>LibraryMath.mch</tt> | ||
* <tt>LibraryStrings.mch</tt> | * <tt>LibraryStrings.mch</tt> | ||
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:
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. For COS this would be cos = %x.(x:NATURAL|COS(x)). Observe that for Atelier-B this is a tautology. For ProB, the use of such a constant allows one to have a real B function representing the external function, for which we can compute the domain, range, etc.
In a first instance we have predefined a series of external functions and grouped them in various library machines and definition files: