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

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...