An example with SEES and INCLUDES

MACHINE
trucContexte
SETS
AA
END

MACHINE
trucM1
SEES
trucContexte
VARIABLES
var
INVARIANT
var <: AA
INITIALISATION
var := AA
OPERATIONS
trucM1op =
ANY ens WHERE ens <: AA THEN
var := ens
END
END

MACHINE
trucM2
INCLUDES
tien.trucM1, mon.trucM1
OPERATIONS
optrucM2 =
BEGIN
tien.trucM1op ||
mon.trucM1op
END
END

Type check and proofs ok with Atelier B

Composition with SEES and INCLUDES