How To Use B Compiler

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

M1_i.imp

  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

We get

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:

Archives