Problème en langage B

Fermé
zakariuz Messages postés 1 Date d'inscription mercredi 5 juin 2013 Statut Membre Dernière intervention 5 juin 2013 - 5 juin 2013 à 23:17
bonjour/bonsoir tout le monde . je suis débutant en langage(méthode) B , j'ai besoin de faire un raffinement et une implementation manuelle pour ma machine
MACHINE
porte
SETS PORTE ; POS = {ouverte, fermee}
VARIABLES position
INVARIANT position : PORTE -->POS
INITIALISATION
position := PORTE * {fermee}
OPERATIONS
ouverture(pp) =
PRE pp : PORTE
THEN position(pp) := ouverte
END;
fermeture(pp) =
PRE pp : PORTE
THEN position(pp) := fermee
END
END

Merci.