Podstawy Inżynierii Oprogramowania - OCL

Operacje w OCL dla kolekcji używane na ćwiczeniach:

C -> including (el | wyr(el))): collection - dodawanie element do zbioru

C -> includes (el | wyr(el)) : Boolean - sprawdza, czy zawiera zadany element

C -> includesAll (el | wyr(el)) : Boolean - sprawdza, czy zawiera zadany element

C ->excluding (el | wyr(el))): collection - usuwanie elementu ze zbioru

C -> excludes (el | wyr(el)) : Boolean - sprawdza, czy nie zawiera zadanego elementu

C -> excludesAll (el | wyr(el)) : Boolean - sprawdza, czy nie zawiera zadanego elementu

C -> forAll (el | pred(el) : Boolean - sprawdza, czy predykat jest spełniony dla każdego element

C -> exists (el | pred(el)) : Boolean - sprawdza, czy predykat jest spełniony przynajmniej dla jednego elmentu

C -> one (el | pred(el)) : Boolean - sprawdza, czy istnieje dokładnie jeden element, dla którego spełniony jest predykat

C -> isUnique (el | wyr(el)) : Boolean - sprawdza, czy dla każdego element wartość jest inna

C -> forAll (e1, e2 | e1 <> e2 implies wyr(e1) <> wyr (e2) : Boolean

C ->select (el | pred(el)) : collection - zwraca kolekcję elementów spełniających zadany warunek

C ->reject (el | pred(el)) : collection - zwraca kolekcję elementów nie spełniających zadanego warunku

C -> collect (el | wyr(el)): collection - kolekcja któregoś z atrybutów

C.Własność

C -> sum (): Integer lub Real - dodaje wartości elementów

C -> sortedBy (el | wyr(el))) - sortowanie rosnące

C -> any (el | pred (el)): object - zwraca jeden losowy element

C -> first (): object - zwraca pierwszy element kolekcji

C -> last (): object - zwraca ostatni element kolekcji

Przykład z ćwiczeń (księgarnia internetowa)

Cena książki jest dodatnia (inwariant):

context Książka

inv: cena > 0

Wszyscy klienci księgarni są unikalni po nazwisku (inwariant):

context Księgarnia

inv: kl -> isUnique (naz)

Klienci mają tylko książki należące do naszej księgarni (inwariant):

context Księgarnia

inv: ks -> includesAll (kl.ks)

Definiowanie reguł dla funkcji:

Uwaga 1: ‘body’ (blok ciała funkcji) jest jednoznaczny z wyrażeniem ‘result’ w bloku ‘post’

Uwaga 2: ‘body’/’reult’ można zastosować tylko wtedy, gdy:

- jest to czysta funkcja (nie zmienia stanu)

- ma jednoznacznie określony wynik

- potrafimy podać wyrażenie (… - braki w notatkach)

Uwaga 3: gdy brak warunków początkowych, to należy pominąć blok ‘pre’

Uwaga 4: jeśli blok ‘post’ ma postać ‘result = …’, to należy go pominąć

Wartość wszystkich książek zakupionych przez osobę:

context Osoba::wart() : Real

body: ks.cena -> sum()

lub context Osoba::wart() : Real

post: reult = ks.cena -> sum()

Daj klienta o zadanym nazwisku:

context Księgarnia::daj(n:Nazwisko): Osoba

pre: kl.naz -> includes (n)

body: kl -> any (nazw = n)

Daj zbiór książek zakupionych przez klienta:

context Osoba::coKupował(): Set(Tytuł)

body: ks.tyt -> asSet

Wartość wszystkich książek księgarni:

context Księgarnia::Wart(): Real

body: kl.wart() -> sum()

Katalog książek, które mieliśmy w księgarni:

context Księgarnia::katalog(): Set (Tyt)

body: ks.tyt -> asSet

Zbiór książek dostępnych do sprzedaży:

context Księgarnia::doSprzedania(): Set(Książka)

body: ks -> reject (k | kl.ks -> includes (k))

lub context Księgarnia::doSprzedania(): Set(Książka)

body: ks – kl.ks -> asSet | Uwaga: można, bo żadna książka nie jest sprzedana więcej niż 1 raz

Daj niesprzedaną książkę o zadanym tytule:

context Księgarnia::dajKsiazke (t: Tytuł): Książka

pre: doSprzedania() -> exists (k | k.tyt = t) |Uwaga: lub … -> exists (tyt = t)

post: doSprzedania() -> select (tyt = t) -> includes (result)

lub context Księgarnia::dajKsiazke (t: Tytuł): Książka

pre: doSprzedania().tyt -> includes (t)

post: doSprzedania() -> select (tyt = t) -> includes (result)

Kto kupił książkę o podanym tytule:

context Księgarnia::ktoKupował (t: Tyt): Set(Osoba)

body: kl -> select (ks -> exists (tyt = t))

lub context Księgarnia::ktoKupował (t: Tyt): Set(Osoba)

body: kl -> select (coKupował() -> includes(t))

Dodanie nowego klienta:

context Księgarnia::nowyKlient (k: Osoba)

pre: kl.naz -> exludes (k.naz)

post: kl = kl@pre -> including (k) |Uwaga: @pre oznacza wartość przed rozpoczęciem

Daj klienta, który wydał najwięcej pieniędzy:

context Księgarnia::najlepszy(): Osoba

pre: kl -> notEmpty()

post: kl -> includes (result)

post: result.wart() = kl.wart() -> sortedBy (w | w) -> last()