In this chapter, we only address the way to use the B Compiler executable file. Embedding the B Compiler library in an application is presented in another section.
Considering the files M1.mch and M1_i.imp given below:
- M1. mch
MACHINE M1 VARIABLES XX INVARIANT XX:INTEGER INITIALISATION XX:=0 OPERATIONS OP1 = BEGIN XX:=1 END; OP2 = SELECT XX=0 THEN XX:=1 END END
IMPLEMENTATION M1_i REFINES M1 CONCRETE_VARIABLES XX INVARIANT XX:INTEGER INITIALISATION XX:=0 OPERATIONS OP1=BEGIN XX:=0 END; OP2=BEGIN XX:=0 END END
To use the B Compiler, just type in:
bcomp -i M1.mch
If the tool doesn’t produce any message, it means that the M1.mch file is parsed without any error. The option -v can be used to make the tool a bit more verbose:
bcomp -v -i M1.mch
The tool then generates the following messages:
Doing syntax analysis for component M1.mch Using path "./M1.mch" for component M1.mch
We can also perform a semantic analysis on the implementation M1_i.imp. In this case, the B compiler will load the implementation then its specification.
bcomp -v -a -i M1_i.imp
Doing syntax analysis for component M1_i.imp Using path "./M1_i.imp" for component M1_i.imp Doing semantic analysis for component M1_i Doing syntax analysis for component M1.ref Using path "./M1.mch" for component M1.mch
Several options are available and are described in another section: