Boolean Expression
5.1 Specyfikacje oparte na stanach
Specyfikacje oparte na stanach opisują systemy oprogramowania w kategoriach stanów i efektów operacji na stanach. Takie specyfikacje są obsługiwane przez kilka języków specyfikacji, które zgrupowaliśmy w dwie grupy: klasyczne języki specyfikacji, takie jak Z, B i VDM oraz języki asercji, takie jak Eiffel, JML (Java Modeling Language) i tablice Petersa i Parnasa. Podczas gdy klasyczne języki specyfikacji definiują stany i przejścia niezależnie od implementacji, języki asercji określają stany i przejścia jako deklaracje lub adnotacje programu źródłowego.
Specyfikacje oparte na stanach są używane jako oracje testowe poprzez weryfikację zgodności wykonania testu ze specyfikacją. Główny problem w generowaniu wyroczni testowych ze specyfikacji opartych na stanach wynika z różnych poziomów abstrakcji pomiędzy specyfikacjami a operacjami monitorowanymi podczas wykonywania testu; dlatego specyfikacje operacji będą tłumaczone w formie sprawdzalnej. Języki specyfikacji są zazwyczaj wystarczająco ekspresyjne, aby reprezentować różne struktury danych i właściwości oparte na stanach, ale ich ekspresyjność komplikuje tłumaczenie na formę wykonywalną. Często w tłumaczeniu przyjmuje się pewne założenia upraszczające, takie jak ograniczenie zbiorów nieskończonych, na przykład nieskończonego zbioru liczb naturalnych, oraz obsługa elementów niewykonywalnych tylko częściowo i czasami wymagająca pewnej interwencji człowieka.
W tym miejscu omówimy główne podejścia do tłumaczenia specyfikacji stanowych na postać wykonywalną. Tłumaczenie specyfikacji Z, B i VDM przedstawia te same problemy związane z nieskończonymi strukturami danych, częściowo zdefiniowanymi wyrażeniami i strukturami obiektowymi. Tłumaczenie Eiffel, JML i innych języków asercji do postaci sprawdzalnej przedstawia podobne problemy, ale na innym poziomie abstrakcji. W dalszej części przedstawiamy główne podejścia do tłumaczenia specyfikacji opartych na stanach do postaci sprawdzalnej w odniesieniu do języka Z; podejścia dla innych języków są podobne. Następnie omawiamy problemy kompilacji asercji do postaci wykonywalnych sprawdzeń odnoszących się do Eiffla, JML-a oraz tablic Petersa i Parnasa.
Kompilator predykatów schematu zaproponowany przez Mikka kompiluje specyfikacje Z do kodu C. Dla każdego schematu Z, który jest podstawową jednostką w Z, podejście to generuje funkcję C, która ocenia predykaty schematu używając stanu programu przekazanego do funkcji jako parametr. Wygenerowany kod ocenia predykaty schematu za pomocą strategii „brute force”: Biorąc pod uwagę stan, kod zasadniczo zastępuje wyrażenia ich wartościami, ocenia formuły rachunku propozycjonalnego za pomocą tablic prawdy oraz ocenia kwantyfikatory i konstrukcje zbiorów poprzez iteracje po strukturach danych. Aby zredukować złożoność generowanych funkcji C, podejście proponuje krok optymalizacji, który zapewnia, że generowany kod C zawsze się kończy. Aby zoptymalizować kod, technika ta definiuje „wykonywalny” podzbiór języka Z. Podzbiór ten składa się z predykatów skończonych. Podzbiór ten składa się ze skończonych predykatów, takich jak formuły rachunku propozycjonalnego, kwantyfikatory na skończonych zbiorach oraz konstrukcje zbiorów oparte na skończonej iteracji. Technika ta rozszerza zbiór wykonywalnych predykatów o zestaw reguł do przekształcania specjalnych niewykonalnych predykatów, które spełniają pewne warunki, w predykaty wykonywalne bez zmiany ich semantyki. Na przykład, następujące dwie reguły eliminują kwantyfikatory:
gdzie M jest zbiorem, zmienna x reprezentuje element w M, a P jest predykatem. Operator -, znany również jako „plamka notacji Z”, oznacza „taki, że”, gdy jest używany z kwantyfikatorem ∃ i „że”, gdy jest używany z kwantyfikatorem ∀. Na przykład, ∃ x : M – P oznacza, że istnieje co najmniej wartość x w M taka, że predykat P jest prawdziwy. Warunek NotOccur(x, P) wskazuje, że x nie jest zmienną wolną w predykacie P. Chociaż zbiór M może być nieskończony, kompilator może nadal kompilować specyfikacje używające kwantyfikatorów nad M tak długo, jak kwantyfikatory mogą być wyeliminowane przez zastosowanie powyższych reguł. W przypadku funkcji definiowanych przez użytkownika, które mogą być wprowadzone przez definicje aksjomatyczne lub generyczne, kompilator wymaga od użytkownika dostarczenia odpowiedniego kodu. Mikk proponuje również rozwiązanie problemu częściowo zdefiniowanych specyfikacji. Używa on VDM-SL jako formy pośredniej oraz kompilatora VDM-SL opracowanego przez Schmidta i Hörchera do tłumaczenia specyfikacji Z na kod C . Kiedy mamy do czynienia z częściowo zdefiniowanymi wyrażeniami, tj. albo funkcjami lub relacjami, które mogą oceniać niezdefiniowane (oznaczane jako ⊥), gdy są oceniane poza ich domeną definicji, podejście generuje obsługę wyjątków.
Obiektowo zorientowane rozszerzenia Z, takie jak Object-Z, pogłębiają problemy. McDonald et al. tłumaczą specyfikacje Ojbect-Z klas kontenerów na kod C++ w trzech etapach: optymalizacji, mapowania strukturalnego i tłumaczenia predykatów. Na etapie optymalizacji zmieniają oni specyfikację w celu uproszczenia późniejszego tłumaczenia poprzez kilka kroków, w tym zastąpienie zmiennych stałych ich wartościami oraz usunięcie zmiennych wtórnych i elementów wzbogacających schemat. Na etapie mapowania strukturalnego, mapują struktury w specyfikacji Object-Z na odpowiadające im elementy kodu: Stałe i zmienne specyfikacji na zmienne z odpowiednimi inicjalizacjami, a typy zmiennych na prymitywne typy C++ lub odpowiadające im klasy w bibliotece pakietu narzędziowego Z używanego przez technikę. Na przykład, mapują typy integer i boolean na int, a typ zbiorów integer na z_set<int >. Mapują one schemat inicjalizacji na konstruktor, a schematy operacji na funkcje członkowskie, tworzą specjalną funkcję członkowską, inv(), do sprawdzania niezmienności klasy i generują klasę wyjątków dla każdego schematu wyjątków.
W tłumaczeniu predykatu DeepL, technika skupia się na tym, jak wygenerować kod do sprawdzania stanu programu, zamiast oceniać predykaty. Na przykład, tłumaczenie uniemożliwia funkcji inv() wywołanie jakiejkolwiek innej funkcji członkowskiej, aby uniknąć nieskończonej rekurencji. W konstruktorze, niezmiennik klasy jest sprawdzany przy jego wyjściu.
Richardson et al. koncentrują się na systemach krytycznych czasowo, zajmują się kombinacją logiki Z i logiki przedziałów czasowych, i proponują tłumaczenie specyfikacji na wyrocznie testowe za pomocą interpretacji symbolicznej. Interpretacja symboliczna przypisuje nazwy symboliczne w specyfikacji do wejść bodźców i zmiennych stanu początkowego, poprzez odniesienie do map danych i sterowania. Następnie interpretacja symboliczna interpretuje każdą ścieżkę sterowania w specyfikacji, to znaczy tworzy asercję wyrażającą warunek na danych specyfikacji w oparciu o stan symboliczny w każdym punkcie kontrolnym specyfikacji. Punkt kontrolny specyfikacji jest odpowiednim elementem, takim jak sparametryzowane zdarzenie, przejście i operacja. Po symbolicznej interpretacji specyfikacji Z, informacja o wyroczni jest reprezentowana jako lista odpowiednich schematów Z i odpowiadających im asercji, które są sprawdzane, jeśli schemat jest wywoływany. Wykonanie przypadku testowego odnosi się do konkretnego wejścia testowego, z którego konkretne zmienne i zdarzenia są wiązane do ich odpowiedników w klasie testowej (każda klasa testowa jest partycją wejścia testowego). Wykonanie przypadku testowego tworzy profil wykonania, a konkretne zdarzenia i wartości zmiennych zawarte w profilu wykonania są mapowane na poziom wyroczni w celu sprawdzenia ich zgodności z informacjami o wyroczni.
Języki asercji łączą specyfikacje z kodem źródłowym, co upraszcza, ale nie eliminuje problemu tłumaczenia. Asercje są wspierane przez różne języki i metodologie. Projektowanie przez kontrakt jest paradygmatem projektowania oprogramowania, który postuluje wspólne projektowanie kodu i asercji. Projektowanie przez kontrakty zostało zaproponowane przez Meyera i jest w pełni wspierane przez język programowania Eiffel. W odróżnieniu od ogólnych języków specyfikacji, takich jak Z, specyfikacje w Eiffel, zwane kontraktami, są wtopione w kod źródłowy i definiują zobowiązania i korzyści komponentów oprogramowania, które komunikują się za pomocą dobrze zaprojektowanych interfejsów. W językach wspierających kontrakty, zobowiązania i korzyści klienta są wyrażone jako warunki wstępne i wtórne dostawców usług. Kod źródłowy jest wzbogacony o inwarianty reprezentujące właściwości stanu, które muszą być zachowane podczas każdej interakcji.
Kontrakty zostały rozszerzone na wiele języków. iContract jest pierwszym narzędziem wspierającym kontrakty w Javie. W iContract kontrakty są zapisywane jako komentarze do kodu za pomocą specjalnych znaczników. Kontrakty obsługiwane przez iContract są wyrażeniami boolean zgodnymi ze składnią Javy, z wyjątkiem kilku rozszerzeń składniowych, do których należą kwantyfikacja uniwersalna (∀), kwantyfikacja egzystencjalna (∃) oraz implikacja (→). Rozszerzenia te mają na celu uproszczenie ich tłumaczenia na kod Javy. Na przykład, the syntax of ∀ is forall < Class >< var > in < Enum >< Exp_var >, where < Class > is the type of the variable < var >, which represents an element of < Enum >. A reasonable translation of the ∀ expression is to use a Java loop to iterate over the enumeration < Enum > and evaluate the boolean expression < Exp_var > in each iteration. The existential quantification is translated similarly. An implication expression C implies I can be simply translated into an if statement: „if C then check I.”
Poza prostym tłumaczeniem wyrażeń boolean, iContract porusza kwestie związane z cyklem życia obiektu, zakresem zmiennych oraz dziedziczeniem, z których większość jest specyficzna dla programowania obiektowego. Najważniejsze reguły związane z cyklem życia obiektu są następujące:
W konstrukcji obiektu warunki wstępne muszą być sprawdzone na początku konstrukcji, natomiast inwarianty i warunki końcowe są sprawdzane tylko wtedy, gdy konstrukcja zakończy się normalnie (bez wyjątków).
W przypadku normalnych wywołań metod na obiektach, warunki wstępne i końcowe są sprawdzane na wejściu i wyjściu wywoływanych metod, a inwarianty nie są sprawdzane dla metod prywatnych.
W destrukcji obiektu sprawdzanie nie jest wymagane. Dlatego do metod finalize() nie wstawia się kodu sprawdzającego.
Predykaty używane w postwarunkach często odwołują się zarówno do wartości zwracanej przez metodę, jak i do „starej” wartości (lub „wartości wejściowej”) niektórych zmiennych. iContract syntetyzuje pseudo-zmienną, zwaną return, aby reprezentować wartość zwracaną, przechowuje wartości zmiennych na wejściu i udostępnia je jako nazwy zmiennych z postfiksem @pre. wyrażenia, ich referencje do obiektów są przechowywane bezpośrednio. iContract pozwala na wywoływanie metod członkowskich w kontraktach. W rezultacie może dojść do potencjalnych nieskończonych rekurencji przy sprawdzaniu inwariantów. Aby rozwiązać ten problem, iContract śledzi głębokość rekurencji dla każdego obiektu w każdym wątku i sprawdza tylko inwarianty o głębokości 0. Mechanizmy rozszerzania typów w Javie mają kilka implikacji na to, jak powinny być obsługiwane kontrakty typów. iContract propaguje kontrakty zgodnie z następującymi regułami:
Warianty są koniunkcyjne, to znaczy, że inwariant podtypu jest koniunkcją inwariantów wszystkich jego nadtypów.
Postconditions are conjuncted, that is, the postcondition of a subtype is the conjunction of the postconditions of all its supertypes.
Preconditions are disjuncted, that is, the precondition of a subtype is the disjunction of the preconditions of all its supertypes.
JML jest popularnym językiem specyfikacji behawioralnej, który wspiera Design by Contract w Javie . Kontrakty JML są w formie specjalnych komentarzy w Javie. JML wyraża warunki wstępne, warunki końcowe i inwarianty jako wyrażenia boolean poprzedzone słowami kluczowymi requires, ensures i invariant, odpowiednio, i używa wbudowanej metody old(x) do reprezentowania wartości x przed operacją. Podobnie do notacji ▵ w Z, JML używa słowa kluczowego modifies do wskazania zmiennych, które są zmieniane w ciele metody. Ponadto, JML zajmuje się kilkoma cechami obiektowymi, takimi jak widoczność i dziedziczenie.
JML jest podstawą wielu podejść do generowania wyroczni testowych. Bhorkar zaproponował technikę tłumaczenia kontraktów JML na asercje Javy. Chociaż obsługuje tylko warunki wstępne, technika ta odnosi się do kwestii związanych ze zmiennymi tylko w specyfikacji, rafinacją, dziedziczeniem specyfikacji i prywatnością. Podobnie jak iContract, technika ta obsługuje dziedziczenie kontraktów poprzez łączenie i rozłączanie kontraktów w zależności od ich typów. Technika ta używa również tablicy hash (per wątek) w celu uniknięcia rekurencji w sprawdzaniu runtime. Wyrażenia używające kwantyfikatorów są traktowane przez tę technikę jako niewykonywalne i dla takich wyrażeń nie jest generowany kod Java.
Korat zaproponował technikę generowania zarówno przypadków testowych jak i wyroczni ze specyfikacji JML. Technika Korata generuje przypadki testowe z warunków wstępnych i inwariantów, a oracje z warunków następczych i inwariantów. Araujo et al. rozszerzyli JML o kontrakty współbieżne i zaproponowali wsparcie runtime, aby umożliwić sprawdzanie w czasie rzeczywistym asercji, które określają właściwości współbieżne.
Peters i Parnas wprowadzili podejście do generowania wyroczni testowych z formalnej dokumentacji. Dokumentacja ta jest podana w postaci tabelarycznej, która składa się z relacji określających interfejsy procedur i jest tłumaczona na oracle w kodzie C i C++. Podstawowym elementem dokumentacji formalnej są wyrażenia predykatowe zapisane w wariancie logiki predykatowej ze specjalnymi konstrukcjami do obsługi funkcji częściowych. Podobnie do innych technik wyroczni opartych na specyfikacji, technika ta traktuje kwantyfikatory ograniczając je do zbiorów skończonych.
Aby umożliwić iteracje po zbiorach elementów z kwantyfikatorami, Peters i Parnas wprowadzają indukcyjnie zdefiniowane predykaty. Dla zbioru S (który ma być używany w kwantyfikatorach), indukcyjnie zdefiniowany predykat P jest zdefiniowany z trzema elementami I, G i Q. Początkowy zbiór I zawiera skończoną liczbę elementów, G jest funkcją, zwaną „funkcją generatora”, która generuje elementy w zbiorze, a Q jest predykatem, który charakteryzuje własności zbioru. Zbiór S jest zdefiniowany jako najmniejszy zbiór skonstruowany w poniższych krokach indukcyjnych:
S0 = I
Sn + 1 = Sn ∪ {G(x)|x ∈ Sn ∧ Q(x)}
I, G i Q muszą być zdefiniowane tak, aby spełniały specjalny warunek, który zapewnia, że skonstruowany zbiór S jest skończony.
Peters i Parnas proponują podejście do tłumaczenia tabelarycznych dokumentacji na kod C . Ponieważ postać wyrażeń używanych w dokumentacji jest dobrze zdefiniowana, tłumaczenie odbywa się systematycznie.
Inne specyfikacje oparte na stanach są również używane do wyprowadzania wyroczni testowych. Modele UML są na ogół nieformalne, niemniej jednak Bouquet et al. zdefiniowali podzbiór UML 2.1, nazwany UML-MBT, który jest wystarczająco precyzyjny do automatycznego generowania przypadków testowych. UML-MBT zawiera diagramy klas, maszyny stanów oraz podzbiór OCL 2.0. Bouquet et al. używają specyfikacji napisanych w VDM-SL do generowania wyroczni testowych.