On rappelle qu'une pile est une structure de données simple, respectant le principe LIFO (« Last In First Out »), c'est-à-dire que l'on accède toujours au dernier élément que l'on vient d'ajouter à cette structure.
Type Abstrait : Pile
Utilise : Booléen, Elément
Opérations :
créer : → Pile
empiler : Pile × Elément → Pile
sommet : Pile ⇀ Elément
reste : Pile ⇀ Pile
estVide : Pile → Booléen
insérerFin : Pile × Elément → Pile |
On tient compte ici des opérations de base de la pile, ainsi que de l'opération « insérerFin » permettant d'insérer un élément à la fin de la pile (cette opération nous permettra de présenter la récursivité en type abstrait). Le symbole « ⇀ » signifie que l'opération est soumise à des pré-conditions.
On a ici un constructeur : créer ; trois transformateurs : empiler, reste et insérerFin ; et deux observateurs : sommet et estVide. L'opération « empiler » est considérée par certains comme un constructeur car on constate que toute pile est de la forme « empiler(p,e) » ou « créer() ».
Pré-conditions : p ∈ Pile
défini(sommet(p)) ⇒ ¬estVide(p)
défini(reste(p)) ⇒ ¬estVide(p) |
Ces pré-conditions correspondent au fait que l'on ne peut pas « voir » le sommet ou prendre le reste d'une pile vide.
Axiomes : p ∈ Pile e, f ∈ Elément
(P1) sommet(empiler(p,e)) = e
(P2) reste(empiler(p,e)) = p
(P3) estVide(créer()) = vrai
(P3) estVide(empiler(p,e)) = faux
(P4) insérerFin(créer(),e) = empiler(créer(),e)
(P5) insérerFin(empiler(p,f),e) = empiler(insérerFin(p,e),f) |