/* -----------------------------------------------
   (c) Projet NaBLa - Fevrier 2001
   Types de données classiques
   Pile - C.Attiogbe
   Version  GENERIQUE
-------------------------------------------------*/
MACHINE PileGen
SETS    PILE     /* toutes les piles imaginables */
CONSTANTS
       XX        /* ensemble abstrait pour les element de la pile */
ABSTRACT_CONSTANTS
        pvide, top, pop, push
        /* pilevide, tete, enlevertete, ajouterelt */
PROPERTIES
        pvide : PILE
&       top : PILE +-> XX
&       pop : PILE +-> PILE
&       push : XX * PILE --> PILE
/* puis les proprietes de pop, push */
&       !(elt, pp).(elt : XX & pp : PILE =>
          top(push(elt,pp))=elt)
&       !(elt, pp).(elt : XX & pp : PILE =>
          pop(push(elt, pp)) = pp)
/*      +++ axiomes         */

/* maintenant la machine à la B :etat + operation */
VARIABLES 
        pile      /* un etat : une pile */
INVARIANT
        pile : PILE
INITIALISATION
        pile := pvide
OPERATIONS
res <--	TOP = 
	PRE pile /= pvide
	THEN
	   res := top(pile)
	END
;
        PUSH(elt) =  /* ajouter elt à la pile */
        PRE  elt : XX
        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
/* ------------------------------------------ */