No edit summary |
No edit summary |
||
| Line 7: | 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). Suppose we want to declare an external cosinus function named <tt>COS</tt>, then this definition could be <tt>COS(x) == cos(x)</tt>. | ||
* one definition declaring the type of the function. For <tt>COS</tt> this would be <tt>EXTERNAL_FUNCTION_COS == INTEGER --> INTEGER</tt>. | * 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 | ||
| Line 14: | Line 14: | ||
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>: defining sin, cos, tan, sinx, cosx, tanx, logx, gcd, msb, random as well as access to all other Prolog built-in arithmetic functions. | ||
* <tt>LibraryStrings.mch</tt> | * <tt>LibraryStrings.mch</tt>: functions manipulating B STRING objects by providing <tt>length</tt>, <tt>append</tt>, <tt>split</tt> and conversion functions <tt>chars</tt>, <tt>codes</tt>. | ||
* <tt>LibraryFiles.mch</tt>: various functions to obtain information about files and directories in the underlying file system | |||
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: