OCL (Object Constraint Language) pour la pile dans le package java.util

J'ai un examen à venir et je regarde les articles précédents pour avoir une idée de ce à quoi s'attendre. Je suis un peu coincé sur le suivant et j'apprécierais vraiment que quelqu'un puisse donner des exemples de réponses.

Écrivez les conditions préalables et postconditions dans OCL pour chacune des opérations suivantes (incluses dans la classe Stack du package java.util):

• (1) Boolean empty () - Teste si cette pile est vide
• (2) E peek () - Regarde l'objet en haut de cette pile sans l'enlever de la pile
• (3) E pop () - Supprime l'objet en haut de cette pile et renvoie cet objet comme valeur de cette opération
• (4) E push (E item) - pousse un objet en haut de cette pile

Ici E désigne le type d'éléments dans la pile.

Mes tentatives sont les suivantes:

Boolean empty()
pre: none
post: self -> IsEmpty() = true
//should this be result -> IsEmpty() = true because it returns a boolean value?

E peek()
pre: self -> NotEmpty() = true
post: result = ??? 
// I lose hope at this stage. 

Je ne sais pas non plus si je devrais référencer les éléments de la pile. Par exemple: self.elements -> IsEmpty () = true

Si quelqu'un pouvait m'aider, je l'apprécierais vraiment.

ÉDITER

Un ami a les idées suivantes:

context Stack empty()
pre: self.data.size = 0

context Stack peek()
pre: self.data.AsSequence.first

context Stack pop()
pre: !self.data.isEmpty
post: self.data.AsSequence.first.remove (not sure about this one)
post: self.data.count = @pre:data - 1

context Stack push(E Item)
post: self.data.asSquence.prepend(E.asSequence)
post: self.data.size = @pre.data.size + 1

Les pré- et post-conditions sont un contrat.

• La condition préalable est la partie du contrat que l'appelant doit respecter. Si la condition préalable n'est pas remplie, truela fonction doit générer une erreur.
• La postcondition est la partie du contrat qui doit être remplie par la fonction et décrit la modification attendue de l'objet / du monde. Si la postcondition n'est pas truela mise en œuvre a un bogue.

Les pré- et post-conditions doivent être des expressions booléennes.

Prenons empty?un exemple. Cette fonction peut toujours être appelée, il n'y a donc pas de condition préalable. Et la fonction n'a aucun effet secondaire donc il n'y a pas de postcondition.

Prenons popun autre exemple. Si cette fonction lève une exception sur une pile vide, la condition préalable est self.size > 0, en revanche, si la fonction retourne nilsur une pile vide, il n'y a pas de condition préalable. Les deux sont des choix de conception valides, pas familiers avec le choix de Java. Dans les deux cas, la postcondition est due à self.size = previous.size - 1l'effet secondaire contractuel de la suppression d'un élément.

Etc …

NB, pseudo-code utilisé car non familier avec OCL.