Pour essayer l'INCLUDES

avec l'Atelier B, un petit exemple

MACHINE
contexte
SETS
ENTITE = {truc, machin}
CONSTANTS
rr
PROPERTIES
rr = {(1|->truc), (2 |->machin)}
END

MACHINE
laMienne
VARIABLES
var
INVARIANT
var : 0..100
INITIALISATION
var :: 1..100
OPERATIONS
op(mt) =
PRE
mt : 0..100 &
(var + mt) : 0..100
THEN
var := var + mt
END
END

MACHINE
incluante(ent1, ent2)
CONSTRAINTS
ent1 : ENTITE & ent2 : ENTITE & ent1 /= ent2
SEES
contexte
INCLUDES
ent1.LaMienne, ent2.LaMienne
OPERATIONS
opAppelante (mt) =
PRE
mt : NAT
THEN
ent1.op(mt) ||
ent2.op(mt)
END
END

Typez, prouvez...