Podstawowe konstrukcje
Opisane konstrukcje odnosić się będą do poniższego diagramu klas:
Niezmienniki klas
Dla dowolnej klasy można podać jej niezmiennik (ang. invariant) w postaci zbioru wyrażeń. Każde wyrażenie niezmiennicze jest wyrażeniem boolowskim, tzn. może być wartościowane jako prawda lub fałsz. Dla więcej niż jednego wyrażenia przyjmuje się, że niezmiennik jest koniunkcją tych wyrażeń. Niezmiennik danej klasy oznacza, że wszystkie obiekty tej klasy spełniają zadany niezmiennik. Niezmiennik oznaczamy słowem kluczowym inv.
context Klient inv:
wiek > 17
wiek < 75
Niezmiennik ten oznacza, że dla wszystkich obiektów klasy Klient wartość atrybutu wiek jest większa od 17 i jest mniejsza od 75.
Odwołania do atrybutów i operacji
W wyrażeniach możemy odwoływać się do wartości atrybutów klasy oraz do rezultatów działania takich operacji, które nie mają skutków ubocznych.
context Klient inv:
self.nazwisko <> '' and self.wiek >= 18
nazwisko <> '' and wiek >= 18
self.wiek() >= 18
wiek() >= 18
self.uprawniony()
uprawniony() and wiek >= 18
Wyrażenie wiek >= 18 dotyczy atrybutu wiek, wyrażenie wiek() >= 18 odnosi się do rezultatu operacji wiek(). Słowo kluczowe self wskazuje na dowolny obiekt zadany przez kontekst (tutaj obiekt klasy Klient). Można je pomijać, o ile wyrażenie pozostaje jednoznaczne.
Odwołanie do obiektu powiązanego przez nawigację
Możemy odwołać się do obiektu na drugim końcu powiązania korzystając z nazwy roli lub z nazwy klasy pisanej małą literą (o ile nazwa klasy określa jednoznacznie dane powiązanie). Odwołując się do atrybutów lub operacji powiązanej klasy używamy notacji kropkowej np.:
context KartaKlienta inv:
właściciel.nazwisko <> ''
klient.nazwisko <> ''
właściciel.wiek() >= 18
ważność and klient.wiek() >=18 and klient.nazwisko <> '' and właściciel.uprawniony()
W ostatnim wyrażeniu występują odwołania zarówno do atrybutu klasy określającej kontekst (ważność z klasy KartaKlienta), jak i atrybutu z klasy dostępnej przez powiązanie (klient.nazwisko). Odwołanie do kolekcji obiektów
Powiązanie może odnosić się do wielu obiektów danej klasy, zgodnie z krotnością zapisaną na końcu powiązania. Odwołania przy użyciu takiego powiązania dotyczą wówczas kolekcji obiektów. Za pomocą operatora kolekcyjnego '->' zapisujemy operacje, które wykonujemy na kolekcji obiektów.
context Klient inv:
karty -> size() <= 5
Niezmiennik określa, że liczba elementów kolekcji (tzn. kart klienta) nie przekracza 5. Size() jest standardową operacją na kolekcji .
Iteracje po elementach kolekcji
Wybrane operacje kolekcyjne (np. select, forAll, exists) obliczają zadane wyrażenie dla wszystkich elementów kolekcji. Możliwe są trzy formy składni tych operacji:
kolekcja -> operacja (element:Typ | )
kolekcja -> operacja (element | )
kolekcja -> operacja ()
Na przykład operacja select sprawdza wszystkie elementy kolekcji i zwraca kolekcję tych elementów, które spełniają zadane wyrażenie boolowskie.
transakcje -> select (a:Transakcja | a.punkty >10)
transakcje -> select (a | a.punkty >10)
transakcje -> select (punkty >10)
W kontekście klasy KartaKlienta wszystkie powyższe wyrażenia wyznaczają zbiór transakcji danej karty, dotyczących więcej niż 10 punktów. Odwołanie poprzez ciąg nawigacji
Korzystając z nawigacji powiązań można odwoływać się do klas (kolekcji ich obiektów) nie powiązanych bezpośrednio z daną klasą.
context Klient inv:
karty.transakcje.punkty -> sum() > 100
Suma punktów ze wszystkich transakcji dla wszystkich kart klienta przekracza 100.
Warunki początkowe i końcowe operacji
Przy projektowaniu według umowy (ang. design by contract) określamy warunki oferowanych usług oraz obowiązki ich dostawcy. Interfejs dostawcy usług wyrażony jest zbiorem operacji. Przed wykonaniem operacji powinny być spełnione warunki początkowe. Po zakończeniu operacji prawdziwe powinny być warunki końcowe. Warunki początkowe i końcowe operacji są zapisywane w kontekście tej operacji jako wyrażenia boolowskie (analogicznie jak niezmienniki dla klas).
context Konto::unieważnijKonto(): Boolean
pre: klient.karty -> exists ( debet() >= maxdebet )
post: punkty = 0 and klient.karty->isEmpty()
Rezultat działania zwracany przez operację
Wartość wynikowa operacji może zostać wyspecyfikowana po słowie kluczowym body. Typ wyrażenia określającego zwracany rezultat musi być zgodny z typem danej operacji.
context Konto::unieważnijKonto(): Boolean
body: punkty = 0
Operator czasu
W warunkach końcowych operacji lub zwracanych rezultatach możemy korzystać z takich wartości atrybutów lub powiązań, jakie były aktualne przed wykonaniem tej operacji. W tym celu dołączamy słowo kluczowe @pre na końcu nazwy odpowiedniego elementu.
context Konto::unieważnijKonto(): Boolean
post: punkty= klient.karty->select(ważność@pre).debet()->sum()
W tej implementacji zakładamy, że punkty w klasie Konto zależą od wielkości debetu na tych kartach klienta, które były ważne przed wywołaniem operacji unieważnijKonto(), a są nadal (po wykonaniu operacji) powiązane z klientem. W wyrażeniu korzystamy z wartości atrybutu ważność z klasy KartaKlienta przed wykonaniem tej operacji.
Ograniczenia początkowe dla atrybutów
Dla atrybutów klas ograniczenia mogą określać wartości początkowe atrybutu (init:).
context Konto::punkty : Integer
init: if klient.wiek > 60 then 100 else 0 endif
Dla każdego obiektu klasy Konto wartość początkowa jego atrybutu punkty wynosi 100, jeśli w obiekcie klasy Klient (powiązanym z danym obiektem klasy Konto) wartość atrybutu wiek jest większa od 60. W przeciwnym razie wartość początkowa atrybutu punkty wynosi 0.
Ograniczenia wyprowadzone dla atrybutów
Dla atrybutów klas ograniczenia mogą określać wartości wyprowadzane (derive:).
context Konto::punkty : Integer
derive: transakcje.punkty -> sum()
W tym przypadku wartość atrybutu punkty w klasie Konto jest równa sumie wartości atrybutu punkty we wszystkich powiązanych z kontem transakcjach.
