The bool operator of B (transforming a predicate into an expression)

Où l'on voit bien la définition de bool

MACHINE
essaiBool
VARIABLES
xx, yy, b1, b2
INVARIANT
xx : 0..5 & y : 0..5 &
xx = yy &
b1 : BOOL & b2 : BOOL & b1 = b2
INITIALISATION
ANY truc WHERE truc : 0..5 THEN
xx := truc ||
yy := truc
END ||
b1:= TRUE ||
b2:= TRUE
OPERATIONS
modif(ee) =
PRE
ee : 0..5
THEN
xx := ee ||
yy := ee
END;
verite=
BEGIN
IF (xx=yy) THEN b1:= TRUE ELSE b1 := FALSE END||
b2 := bool(xx=yy)
END
END