This tutorial describes, how ProB's integrated plugin for unit analysis can be used to verify the usage of physical units throughout a B machine. This includes
The plugin is currently a work in progress. Rough edges are to be expected.
We assume that you have a general understanding of B and the usage of ProB.
Currently, the plugin can only be used with classical B machines. Therefore, a B machine needs to be loaded before the plugin can be activated.
Once a machine is loaded, the plugin can be activated through ProB's plugin menu. Choose "Interpreting units stored in pragmas" inside of the activate plugin submenu. Furthermore, the preferences can be accessed through the menu.
At this stage, two preferences can be set:
If the static pre-check is activated, the plugin moves the animator into a fix point state, in which possible unit errors are presented to the user through ProB's error reporting facilities.
To connect a variable with an expected physical unit, a special comment is placed before the variable.
VARIABLES /*@ unit 10**1 * m**1 */ x, /*@ unit m**2 */ y
Following the "unit" keyword is a specification of the unit in form of a B expression. Allowed constructs are multiplication and division as well as exponentiation.
For several often used units like cm, dm, km, etc. an alias can be used.
VARIABLES /*@ unit mm */ x, /*@ unit dm */ y
Once at least one variable is annotated, further units can be inferred.
The unit plugin integrates with ProB's animation facilities. Both results and parameters of operations are displayed with their unit. For variables, the unit is stored inside the machines state space. This enables the plugin to be used in conjunction with the evaluation view, the dot output and most other ProB features.
To distinct between a numerical multiplication, that changes the values without changing the unit and a multiplication meant to convert between units, a second pragma is added. To convert between units, add the respective conversion factor and mark the multiplication as a unit conversion.
See the following B machine for an example operation:
MACHINE SimpleConversion VARIABLES /*@ unit [-2,m,1] */ xx, /*@ unit [-3,m,1] */ yy, converted INVARIANT xx:NAT & yy:NAT & converted:NAT INITIALISATION xx,yy,converted:=0,0,0 OPERATIONS n <-- addToXX = n:=xx+1; mmToCm = converted:=/*@ conversion */(10*yy) END
If activated, the results of the static analysis can be accessed from the plugin menu. Currently, the results include the inferred unit of every variable inside the active B machine. Furthermore, a warning is displayed, if multiple units were inferred for a single variable (which usually is caused by wrong usage of the variable). Another warning message is shown for variables, for which no unit could be inferred.