Ograniczenia dynamiczne w modelowaniu zachowania obiektów

Model zachowania (działania, dynamiki) obiektów zawiera opis tych aspektów systemu, które dotyczą realizowanych w systemie operacji oraz ich kolejności. W modelu zachowania ujęte są również zdarzenia występujące w systemie oraz wzajemne interakcje obiektów. Przy opracowaniu modelu zachowania wykorzystać można diagramy interakcji, diagramy stanów i aktywności.

Diagramy stanów opisują w formie graficznej zbiór stanów oraz przejść pomiędzy nimi, zdarzeń i wzajemnych interakcji obiektów. Diagramy stanów wzorowane są na mapach stanów Harela [HAREL1985]. Mapy stanów są z kolei rozszerzeniem notacji diagramów automatów skończenie stanowych. Rozszerzenie to obejmuje wprowadzenie hierarchii stanów, równoległości procesów oraz przekazywanie komunikatów.

Praca [MAWI2001] proponuje metodę specyfikacji dynamicznych więzów integralności w obiektowym modelu danych. W niniejszym rozdziale wykorzystamy to rozwiązanie do specyfikacji ograniczeń dynamicznych i konstrukcji na ich podstawie diagramów stanów modelujących poprawne zachowanie obiektów.

Dynamiczne więzy integralności pozwalają na stawianie ograniczeń ponad sekwencją, zwykle uporządkowanych w czasie stanów bazy danych, dotyczą więc przede wszystkim obiektów trwałych. Przez ograniczenia dynamiczne dla obiektów rozumiemy warunki poprawności operacji realizowanych na obiektach odwołujące się nie tylko do pojedynczego stanu obiektów, lecz do sekwencji stanów.

Formuły OCL specyfikują właściwości instancji wskazanego typu. Jeżeli formuły nie stanowią opisu diagramów, z których jednoznacznie wynika jakiego typu dotyczą, wymagane jest wskazanie kontekstu formuły. Deklaracja kontekstu formuły następuje po słowie kluczowym context, po którym wskazać należy nazwę odpowiedniego typu lub wybraną metodę typu. Wyróżniono trzy stereotypy formuł OCL. Wskazanie stereotypu formuły musi być umieszczone bezpośrednio po deklaracji jej kontekstu i następuje poprzez słowa kluczowe oznaczające: inv – inwarianty klasy (w kontekście typu), pre, post – warunki poprawności dla metod i operacji klas (w kontekście metody bądź operacji typu).

Nawigacja poprzez wszystkie dostępne w statycznym modelu systemu klasy, związki, atrybuty i metody następuje poprzez notacje kropkową. Mechanizm ten umożliwia odwołanie się do wszystkich obiektów powiązanych z instancją kontekstową. Poczynając od wybranego obiektu możemy nawigować do powiązanych obiektów i ich własności wskazując etykiety asocjacji powiązanych klas. Predefiniowane typy zbiorowe OCL oferują szereg predefiniowanych właściwości i operacji. Należą do nich między innymi własności: notEmpty - typu logicznego, spełniona, jeżeli zbiór jest pusty, size – ilość elementów zbioru. Dostęp do predefiniowanych własności bądź operacji na kolekcjach uzyskuje się przy użyciu symbolu „->”.

Jeżeli wystąpi potrzeba odwołania się do kolekcji wszystkich instancji danego typu (wszystkich obiektów danej klasy) wówczas możemy wykorzystać predefiniowaną własność allInstances. Należy pamiętać, iż właściwość ta nie jest określona dla niektórych predefiniowanych typów np.: Real, Integer. W przykładzie (2) wykorzystano kolejną predefiniowaną operację na kolekcjach forall – służącą specyfikacji warunków logicznych, które muszą być spełnione dla wszystkich elementów kolekcji.

Rysunek 1. Przykładowa hierarchia klas

(1)  context Wykładowca inv : 
     self.wiek() > 18

(2) context Zajecia inv MaxIloscStudentow
    zajecia.allInstances -> forall( z | 
          z.zapisany_na -> notEmpty implies 
          z.zapisany_na ->size <= z.iloscMiejsc)

Nasza propozycja obejmuje formułowanie ograniczeń ponad skończonymi sekwencjami stanów obiektów na etapie modelowania systemu, a nie w trakcie jego eksploatacji. W związku z tym wprowadzenie zarówno operatorów czasu przeszłego jak i przyszłego nie zwiększyłoby ekspresywności proponowanego języka [EMER1990], [KLIM1999]. Prace z dziedziny dynamicznych więzów integralności w bazach danych nie dają w tej kwestii jednoznacznych rozstrzygnięć, proponują wykorzystanie logiki czasu przyszłego [SALI1988], [LIZH1991], [GELI1996] bądź logiki czasu przeszłego [CHOM1992], [SASCH1992], [CHOM1995]. Obecne w literaturze przekonanie o bardziej naturalnym formułowaniu ograniczeń w logice temporalnej czasu przeszłego [LPZ1985] skłania nas do zaproponowania rozszerzenia języka OCL wyłącznie o zestaw operatorów temporalnych czasu przeszłego. Dodatkowym argumentem za wprowadzeniem operatorów czasu przeszłego jest obecność operatora @pre w języku OCL pozwalającego na odwołanie się do poprzedniej wartości własności obiektów w warunkach post dla operacji. Język OCL nie przewiduje możliwości wykorzystanie operatora umożliwiającego odwołanie się do przyszłych wartości własności obiektów.

W języku ODCL, oprócz standardowych konstrukcji języka OCL, wykorzystywać można także operatory temporalne czasu przeszłego interpretowane następująco:

• prev A - jest spełnione w stanie aktualnym, jeżeli A jest spełnione w poprzednim stanie.

• A since B - jest spełnione w aktualnym stanie, jeżeli istniał stan wcześniejszy, w którym spełnione było B.

• sometime A - kiedyś w przeszłości spełnione było A.

• always A - zawsze w przeszłości spełnione było A.

gdzie: A, B są wyrażeniami logicznymi języka ODCL. Poprzestaniemy tutaj na takim nieformalnym opisie semantyki operatorów temporalnych. Formalną definicję składni i semantyki języka ODCL znaleźć można w pracy [WILCZ2003]. Pełne przedstawienie własności logiki temporalnej znaleźć można w pracy [KLIM1999].

Przy wykorzystaniu języka ODCL można specyfikować formuły odwołujące się do wszystkich elementów, które dostępne są w języku OCL, ze statycznego modelu systemu tj. klas, związków, atrybutów klas, metod. Język ODCL można wykorzystać do specyfikacji inwariantów klas a także warunków pre i post dla operacji i metod.

Dla przykładowej hierarchii klas przedstawionej na rysunku 1. ograniczenie dynamiczne wyrażone w języku naturalnym zdaniem „zanim student zapisze się na zajęcia z przedmiotu Analiza II musi zaliczyć przedmiot Analiza I ” można zapisać w ODCL wyrażeniem postaci:

(3) context Student inv Analiza: 
    let: zapisany(p String):Boolean=
         self.prowadzone_dla->exists(z Zajecia|
                                z.przedmiot.nazwa=p) 
    let: zaliczony(p String):Boolean=
         self.zaliczenie->exists(z Zaliczenie|
                                z.zajecia.przedmiot.nazwa = p
                                and z.ocena > 2) in
    zapisany(‘Analiza II’) implies sometime zaliczony(‘Analiza I’)

Proponowana w tym rozdziale metoda konstruowania diagramów stanów na podstawie specyfikacji dynamicznych ograniczeń w języku ODCL jest adaptacją metod przedstawionych w pracach [SALI1988], [SASCH1992].

Normalizacja formuł języka ODCL polega na ich sprowadzeniu do dysjunkcyjnej temporalnej postaci normalnej, czyli formuły będącej wyłącznie alternatywą podformuł postaci A ∧ prev(B), gdzie A jest podformułą nietemporalną (wyrażeniem logicznym języka OCL) zaś B jest wyrażeniem języka ODCL.

Zwykle normalizację formuły temporalnej rozpoczynamy od wykorzystania praw logicznego rachunku zdań. Implikacja i równoważność zastępowane są odpowiadającymi im konstrukcjami wykorzystującymi alternatywę i koniunkcję. Następnie otrzymana formuła podlega dalszym transformacjom poprzez stosowanie odpowiednich reguł temporalnych dla najbardziej zewnętrznego operatora temporalnego i dalej rekurencyjnie dla pozostałych operatorów, dopóki nie zostaną otoczone operatorem temporalnym prev. Transformacja taka prowadzi do uzyskania formuł złożonych z podformuł nietemporalnych A i podformuł temporalnych prev(B).

Poniższe reguły rekursji temporalnej odpowiadają prawom rekursywnej równoważności klasycznych operatorów temporalnych [KLIM1999], odzwierciedlają semantykę operatorów temporalnych języka ODCL:

gdzie: α, ϕ jest wyrażeniem logicznym ODCL. Dowody powyższych reguł znaleźć można w pracy [WILCZ2003].

Aby zbudować diagram stanów należy formuły zapisane w logice temporalnej czasu przeszłego sprowadzić do postaci normalnej poprzez ich transformacje w teraźniejszą nie temporalną część do sprawdzenia w stanie aktualnym i temporalną część przeszłą z operatorem prev, do weryfikacji w pozostałej sekwencji stanów. Część nie temporalna służy specyfikacji warunku przejścia pomiędzy stanami w diagramach stanów (ang. guards).

Przy danej formule α języka ODCL odpowiadający jej diagram stanów zbudować można realizując następujący algorytm:

• rozpoczynamy od pustego diagramu stanów,

• wstawiamy stan początkowy etykietowany formułą α,

• dla każdego stanu v w diagramie wykonujemy transformacje jego etykiety do dysjunkcyjnej temporalnej postaci normalnej.

• dla każdej uzyskanej podformuły postaci: A ∧ prev(B), jeżeli nie istnieje jeszcze stan etykietowany formułą B, dodajemy nowy stan v’ o etykiecie B, w przeciwnym przypadku podstawiamy pod v’ znaleziony stan etykietowany formułą B

• dodajemy przejście (v, v’) etykietowane formułą A.

• jeżeli pomiędzy stanami v i v’ istnieje więcej niż jedno przejście, zastępujemy je pojedynczym przejściem etykietowanym alternatywą etykiet pierwotnych przejść.

Tak zbudowany diagram stanów nie ma oznaczonych stanów końcowych. Stany końcowe to stany o etykietach danych formułami temporalnymi spełnionymi w pustej sekwencji stanów. Na podstawie semantyki operatorów temporalnych definiujemy funkcję końca K: α → {true, false}, którą wykorzystamy do wyznaczenia zbioru stanów końcowych. Niech ϕ, ψ, ρ będą formułami nietemporalnymi, wówczas:

„zanim student otrzyma wpis zaliczenia zajęć z przedmiotu,

musi zapisać się na dane zajęcia”.

Jego specyfikacja może mieć postać:

(6) context Student inv PSI: 
    let: p:String = ‘PSI’
    let: zapisany(n String):Boolean=
         self.prowadzone_dla->exists(z Zajecia|
                              z.przedmiot.nazwa=n)
    let: zaliczony(n String):Boolean=
         self.zaliczenie->exists(z Zaliczenie|
                              z.zajecia.przedmiot.nazwa=n
                              and z.ocena > 2) in
    zaliczony(p) implies sometime zapisany(p)

(7) zaliczony(p) implies sometime zapisany(p)

Rysunek 2. Przykładowy diagram stanów

(8) not zaliczony(p) or sometime zapisany(p) 

(9) not zaliczony(p) and prev(true) 
     or zapisany(p) and prev(true)
     or true and prev(sometime zapisany(p))

Rysunek 3. Przykładowy diagram stanów

(10) sometime zapisany(p)

(11) zapisany(p) and prev(true) 
      or true and prev(sometime zapisany(p))

Rysunek 4. Przykładowy diagram stanów

Rysunek 5. Przykładowy diagram stanów

Zaproponowane algorytmy konstrukcji diagramów stanów na podstawie specyfikacji dynamicznych więzów integralności można wykorzystać w narzędziach wspierających modelowanie systemów obiektowych w notacji UML. Diagramy uzyskiwane w wyniku zastosowania proponowanych algorytmów po pominięciu temporalnych formuł etykietujących stany diagramu są zgodne z przyjętymi w UML notacjami.