<< 1 Wstęp
Spis treści
3 Metoda Tropów w PVS >>

2 Metoda tropów

2.1 Założenia

Poniższy opis metody tropów jest z konieczności skrótowy, pełny można znaleźć w pracy [4].

Metoda tropów umożliwia specyfikację systemów informatycznych przedstawionych jako zbiór odrębnych, wzajemnie powiązanych modułów. W ramach każdego modułu specyfikuje się interfejs wskazujący możliwe operacje na obiektach definiowanego typu danych (ang. domestic type) i ukrywający wszelkie techniczne szczegóły związane z implementacją (zgodnie z regułą czarnej skrzynki - ang. black-box). Drugim elementem specyfikacji jest projekt implementacji określający zasady implementacji obiektów reprezentowanego typu przy użyciu typów dostępnych standardowo w językach programowania lub projektów interfejsu innych modułów. W ramach metody tropów jest wymagane wykazanie spójności semantycznej projektu interfejsu i projektu implementacji oraz ich wzajemnej odpowiedniości.

2.2 Projekt interfejsu modułu

Metoda tropów pozwala opisać moduły programów z punktu widzenia zewnętrznego obserwatora. Każdy moduł udostępnia zbiór homogenicznych i niezależnych obiektów, które przez programistę powinny być traktowane jako abstrakcyjne typy danych. Każdy obiekt można traktować jak automat w tym sensie, że zewnętrzny obserwator może zauważyć jedynie zdarzenia oddziałujące na obiekt i wyniki generowane w odpowiedzi na te zdarzenia. Pojedynczy obiekt jest definiowany przez następujące własności:

  • posiada stany, podlega zmianom wywołanym przez zdarzenia i przekazuje wyniki,
  • zawsze jest w jakimś stanie, początkowo jest w stanie początkowym,
  • zmiana stanu jest możliwa jedynie jako efekt zdarzenia,
  • wyniki mogą być przekazywane jedynie w odpowiedzi na zdarzenia,
  • co najwyżej jedno zdarzenie może dotyczyć obiektu w danej instancji czasu,
  • zbiór możliwych par złożonych z nastepnego stanu i przekazanego wyniku zależy jedynie od:
    • obecnego stanu,
    • zdarzenia, które oddziałuje na obiekt.

Jedynymi obserwowalnymi własnościami obiektów jest ich zachowanie (wyniki wygenerowane w efekcie zdarzeń) i właśnie historię zachowań danego obiektu nazywamy tropem (ang. trace). Nie każda historia zdarzeń jest poprawnym tropem, więc wprowadza się funkcję określającą tropy sensowne (ang. feasible traces). Tropy sensowne definiowane są następująco: jeśli dla każdego 1 <= i <= n obiekt może wytworzyć wynik Oi w odpowiedzi na zdarzenie Ei po sekwencji zdarzeń i wyników E1.O1.E2.O2....Ei-1.Oi-1, to E1.O1....En.On nazywamy tropem sensownym. Jeśli T i T.S są sensownymi tropami, to S jest sensownym rozszerzeniem tropu T (ang. feasible extension). Relację obserwacyjnej równoważności tropów (ang. observational trace equivalence) określa się w ten sposób, że T1 i T2 są obserwacyjnie równoważne, jeśli mają te same sensowne rozszerzenia.

Moduł opisuje pewną liczbę niezależnych od siebie obiektów. Interakcja pomiędzy światem zewnętrznym a pojedynczym obiektem może się odbywać za pomocą zbioru programów, zwanych programami dostępu (ang. access-programs), które mogą być używane przez inne obiekty w celu pobrania pewnych informacji lub zmian stanu obiektu. Deklaracja programów dostępu zawiera nazwę, opis argumentów i przekazywaną wartość (w przypadku funkcji). Każdemu argumentowi jest przypisany typ oraz deskryptor określający sposób wykorzystania i możliwość modyfikacji argumentu. Wyróżnia się następujące deskryptory (pełna specyfikacja dostępna jest w [4]):

  • "V" - przy wywołaniu programu dostępu jest podana wartość argumentu; wynik wywołania może od niej zależeć,
  • "O" - przy wywołaniu programu dostępu jest podana nazwa obiektu; w wyniku wywołania obiektowi może być przypisana, w sposób deterministyczny, nowa wartość,
  • "R" - przy wywołaniu programu dostępu jest podana nazwa obiektu; w wyniku wywołania obiektowi może być przypisana, w sposób niedeterministyczny, nowa wartość,
  • "VO" - złożenie deskryptorów "V" i "O",
  • "VR" - złożenie deskryptorów "V" i "R".

Aby uprościć identyfikację stanu obiektów stworzono pojęcie tropu kanonicznego (ang. canonical trace) i funkcji rozszerzenia (ang. extension function). Konstrukcja przebiega następująco:

  1. wybieramy pewnien reprezentatywny (z punktu widzenia zewnętrznego obserwatora) podzbiór tropów i nazywamy je kanonicznymi - wszelkie zachowania obiektu będziemy od tej pory opisywać tylko w ramach elementów tego zbioru,
  2. definiujemy relację wyjścia out określającą jakie wyniki mogą być wygenerowane przez obiekt w odpowiedzi na zdarzenie E, gdy dotychczas zaobserwowano ciąg zdarzeń opisany tropem T; jest to jednocześnie definicja zbioru sensownych jednozdarzeniowych rozszerzeń tropów kanonicznych,
  3. definiuje się funkcję rozszerzenia, ef, która przekształca sensowne jednozdarzeniowe rozszerzenia tropów kanonicznych na tropy kanoniczne.

Z definicji zbioru tropów kanonicznych, funkcji rozszerzenia i relacji wyjścia można wywnioskować, które tropy są sensowne. W tym celu definiuje się predykat charakterystyczny tropów sensownych Feasible i funkcję redukującą Reduce, która przekształca tropy sensowne na obserwacyjnie równoważne im tropy kanoniczne.

2.3 Projekt implementacji modułu

Projekt implementacji jest etapem pośrednim w procesie tworzenia oprogramowania, pomiędzy projektem interfejsu i samą implementacją. Odsłania szczegóły implementacyjne modułu (ang. clear-box) w pojęciach struktury danych, która może zawierać obiekty zdefiniowane w innych modułach. Sama ta struktura jest lokalna ze względu na moduł i niewidoczna nigdzie poza nim. Projekt implementacji określa odwzorowanie konkretnych stanów (ang. concrete states) implementowanej struktury danych na stany abstrakcyjne (ang. abstract states) z poziomu projektu interfejsu, a te są reprezentowane przez tropy kanoniczne. Wspomnianą funkcją odwzorowującą jest funkcja abstrakcji (ang. abstraction function), a sam proces przypisywania nowej reprezentacji abstrakcyjnemu typowi danych nazywamy uszczegóławianiem danych (ang. data reification).

Semantyka programów dostępu określonych w projekcie interfejsu modułu jest definowana przez opis zmian dokonanych przez nie na strukturze danych modułu. Wyraża się to przez tzw. LD-relacje [10], które składają się z relacji i zbioru. Relacja opisuje odwzorowanie pomiędzy początkowym a końcowym stanem programu. Zbiór jest kolekcją stanów inicjalnych, dla których gwarantuje się osiągnięcie stanu końcowego.

Projekt implementacji jest zgodny z projektem interfejsu, gdy abstrakcyjne stany używane w obu dokumentach są te same, a funkcja abstrakcji i LD-relacje są zgodne z relacją wyjścia i funkcją rozszerzającą. Zgodność obu projektów można wyrazić za pomocą zbioru obligacji.

W przypadku projektu implementacji opisującego pojedynczy obiekt (ang. single-object) nie ma konieczności określania miejsca przechowywania jego struktury danych, gdyż obiekt jest jeden dla całego modułu. Jednak w projektach wieloobiektowych (ang. multi-object) możliwe są różne formy dzielenia struktury danych pomiędzy klientów a moduł. Z tego względu wyróżnia się trzy rodzaje projektów implementacji:

  • scentralizowane projekty implementacji (ang. centralized internal design): opisują ograniczoną liczbę obiektów, których struktura danych należy do modułu, wszystkie obiekty są tworzone przez moduł przed jakimkolwiek wywołaniem programu dostępu;
  • zdecentralizowane projekty (ang. decentralized internal design): dla każdego obiektu istnieje osobna kopia struktury danych przechowywana po stronie klienta, obiekty są tworzone przez klienta;
  • mieszane projekty implementacji (ang. mixed internal design): struktura danych obiektów jest dzielona pomiędzy klientów i moduł, obiekty są tworzone zarówno przez klienta, jak moduł, przed jakimkolwiek wywołaniem programu dostępu.

Pełny opis projektów implementacji w metodzie tropów można znaleźć w [3].

2.4 Przejście od projektu implementacji do konkretnego języka programowania

Projekt implementacji powinien być pisany pod konkretny, wcześniej wybrany język programowania. W przeciwieństwie do projektu interfejsu, dostępnego dla projektantów i implementatorów innych modułów, jest on szczegółową instrukcją dla programisty ważną jedynie w obrębie modułu. Wyznacza typy danych, z których należy korzystać przy implementacji, określa funkcje pomocnicze konieczne do wyrażenia programów dostępu oraz podaje poprawne wartości początkowe, sposób tworzenia oraz niszczenia obiektów implementowanego typu.

W ogólności zasady transformacji projektu implementacji do kodu w języku programowania są następujące:

  1. Każdy program dostępu jest osobną funkcją.
  2. Każdy argument programu dostępu ma swój odpowiednik wśród parametrów implementowanej funkcji. Sposób przekazywania argumentów zależy od wybranego języka programowania, jednak należy umożliwić przekazywanie wartości poprzez argumenty typu "V".
  3. Funkcje lokalne projektu implementacji (tzn. nie występujące na wcześniejszych etapach specyfikacji) powiny być określone jako prywatne i niedostępne spoza modułu.
  4. Deklarację eksportowanego typu należy umieścić w publicznej części modułu, definicja zaś powinna się znaleźć w prywatnej części kodu.

Jeśli projekt implementacji jest scentralizowany i jest konieczna rezerwacja i zwalnianie obiektów wewnątrz modułu, to należy wymóc na użytkowniku wcześniejszą deklarację struktury, wywołanie konstruktora (któremu w projekcie implementacji odpowiada funkcja) oraz sprawdzenie, czy konstrukcja obiektu powiodła się. Analogicznie za pomocą funkcji należy zorganizowac destrukcję obiektu.

W projekcie implementacji można korzystać z typów danych określonych przez inne moduły, jednak do dyspozycji są jedynie projekty interfejsów. Podczas implementacji analogicznie korzystać można jedynie z publicznych części implementacji innych modułów, gdzie poza deklaracją eksportowanego typu dostępne mogą być jedynie deklaracje funkcji odpowiadających programom dostępu. Umożliwia to zrównoleglenie prac nad modułami i gwarantuje przejrzystość systemu wzajemnych zależności.


<< 1 Wstęp
Spis treści
3 Metoda Tropów w PVS >>