/* -----------------------------------------------
   (c) Projet NaBLa - Fevrier 2001
   Types de données classiques
   Pile - C. Attiogbe - UFR Sciences Nantes
   Version non generique
*/
MACHINE Pile
SETS    PILE     /* toutes les piles imaginables */
ABSTRACT_CONSTANTS
        pvide, top, pop, push
        /* pilevide, tete, enlevertete, ajouterelt */
PROPERTIES
        pvide : PILE
&       top : PILE +-> NAT
&       pop : PILE +-> PILE
&       push : NAT * PILE --> PILE
/* puis les proprietes de pop, push */
&       !(elt, pp).(elt : NAT & pp : PILE =>
          top(push(elt,pp))=elt)
&       !(elt, pp).(elt : NAT & pp : PILE =>
          pop(push(elt, pp)) = pp)
/*      ajouter d'autres axiomes à volonté */

/* maintenant la machine à la B :etat + operation */
VARIABLES 
        pile      /* un etat : une pile */
INVARIANT
        pile : PILE
INITIALISATION
        pile := pvide
OPERATIONS
res <--	TOP =  /* donner le sommet de pile */ 
	PRE
	    pile /= pvide
	THEN
	   res := top(pile)
	END
;
        PUSH(elt) =  /* ajouter elt à la pile */
        PRE  elt : NAT
        THEN
             pile := push(elt, pile)
        END
;
res <-- POP =       /* retirer elt de la pile */
        PRE pile /= pvide
        THEN
           res := top(pile) 
        || pile := pop(pile)
        END
END
/* ---------------------------------------------- */