Object Constraint Language (OCL) dla stosu w pakiecie java.util

Zbliża się egzamin i patrzę na wcześniejsze artykuły, aby dowiedzieć się, czego się spodziewać. Trochę utknąłem w poniższym i naprawdę doceniłbym, gdyby ktoś mógł podać kilka przykładowych odpowiedzi.

Napisz warunki wstępne i dodatkowe w OCL dla każdej z następujących operacji (zawartych w klasie Stack w pakiecie java.util):

• (1) Boolean empty () - Sprawdza, czy ten stos jest pusty
• (2) E peek () - Patrzy na obiekt na górze tego stosu bez usuwania ze stosu
• (3) E pop () - Usuwa obiekt na górze stosu i zwraca ten obiekt jako wartość tej operacji
• (4) E push (E item) - pcha przedmiot na wierzch tego stosu

Tutaj E oznacza rodzaj elementów na stosie.

Moje próby są następujące:

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. 

Nie wiem też, czy powinienem odwoływać się do elementów na stosie. Na przykład: self.elements -> IsEmpty () = true

Gdyby ktoś mógł mi pomóc, bardzo bym to docenił.

EDYTOWAĆ

Przyjaciel ma następujące pomysły:

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

Warunki wstępne i dodatkowe są umową.

• Warunek wstępny jest częścią umowy, którą musi spełnić osoba dzwoniąca. Jeśli warunek nie jest spełniony, truefunkcja musi zgłosić błąd.
• Warunek końcowy jest częścią umowy, którą musi spełnić funkcja, i opisuje oczekiwaną zmianę obiektu / świata. Jeśli warunek nie jest spełniony, truewystąpił błąd.

Zarówno warunek wstępny, jak i końcowy muszą być wyrażeniami logicznymi.

Weźmy empty?jako przykład. Tę funkcję zawsze można wywołać, więc nie ma warunków wstępnych. A funkcja nie ma skutków ubocznych, więc nie ma warunków dodatkowych.

Weźmy popjako kolejny przykład. Jeśli ta funkcja zgłasza wyjątek na pustym stosie, warunkiem jest self.size > 0z drugiej strony, jeśli funkcja zwraca nilna pustym stosie, nie ma żadnego warunku wstępnego. Oba są poprawnymi opcjami projektowymi, nie znającymi wyboru Javy. W obu przypadkach warunkiem jest to, self.size = previous.size - 1że skutkiem ubocznym umowy jest usunięcie elementu.

I tak dalej …

NB, używał pseudo kodu, ponieważ nie zna OCL.