Projektowanie systemów informatycznych (część 6)

Sebastian Wyrwał

Dotychczas omówiono różne zagadnienia związane z inżynierią
oprogramowania i projektowania systemów informatycznych. Zaliczyć do nich można
między innymi modele cykli życia oprogramowania. Przedstawiono również
podział metod projektowania, modelowanie oraz studium wykonalności. Opisano
metody strukturalne oraz obiektowe, w tym język UML. Ważne miejsce w inżynierii
oprogramowania zajmują metody formalne, które omówiono w tym odcinku. Metody
formalne (lub metody im bliskie) mogą być, zdaniem autora, zastosowane wraz z
inżynierią rodzin produktów, lub mówiąc inaczej, zastosowanie tej ostatniej
wymaga pewnej znajomości metod formalnych. Trzeba przyznać, że w polskich
realiach zastosowanie metod formalnych jest dość egzotyczne. Z drugiej strony,
jakość wytwarzanego oprogramowania pozostawia często bardzo wiele do życzenia.
O ile budowa mostu jest poprzedzana wykonaniem projektu i obliczeń i jest to
sytuacja normalna, o tyle w przypadku oprogramowania, naturalna dla większości
osób jest sytuacja, w której się nie projektuje. Jeśli już jakaś firma
decyduje się na projektowanie, są to metody nieformalne lub półformalne;
niezwykle rzadko stosuje się metody formalne. Nie oznacza to oczywiście, iż
każdy system należy specyfikować przy użyciu tych ostatnich. Nie należy ich
jednak z góry odrzucać dlatego tylko, że się ich nie zna. Nie muszą być
one oczywiście stosowane w odniesieniu do całego projektu ale np. do
krytycznych jego części. Niniejszy odcinek omawia język IFAD VDM-SL będący
dialektem języka VDM-SL oraz – bardzo skrótowo – język VDM++.

Na zakończenie tego odcinka pokazano przykłady
automatycznego generowania kodu w języku C++ z prostej specyfikacji funkcji w języku
VDM-SL oraz w języku Java ze specyfikacji klasy w języku VDM++.

Miejsce metod formalnych w przedsięwzięciu programistycznym

Określenie „Formalne metody projektowania” jest
nieścisłe. Jest tak dlatego, że metody te mogą być stosowane w każdej z
faz modelu cyklu życia oprogramowania – począwszy od analizy, poprzez
modelowanie i projektowanie, aż do implementacji i testowania (rys 1.).
Bardziej uzasadniona jest więc nazwa: formalne metody wytwarzania
oprogramowania. W obrębie metod formalnych można spotkać mniejszy lub większy
stopień sformalizowania. W specyfikacji napisanej w języku naturalnym mogą
występować pewne sformalizowane fragmenty. Z drugiej strony może być
specyfikacja całkowicie sformalizowana.


Rys. 1. Metody formalne w procesie wytwarzania oprogramowania

O rodzinach produktów nieco inaczej

Rola metod formalnych w konfiguracji systemu może być do
pewnego stopnia powiązana, zdaniem autora, z koncepcją wytwarzania rodzin
produktów. Warto przypomnieć, iż polega ona na wyodrębnieniu podobnych
produktów i bardzo starannym wytwarzaniu narzędzi służących do generowania
aplikacji w oparciu o ich specyfikację. Obejmuje to zaprojektowanie języka służącego
do opisu aplikacji, specyficznego dla danego typu produktów. Wygenerowana ze
swego opisu aplikacja jest niezmienna tzn. jest konfigurowalna w takim stopniu
jak „normalny” program. Autor widzi możliwość zastosowania metody
różniącej się od omówionej przed chwilą tym, że specyfikacja systemu byłaby
interpretowana. Aplikacja składałaby się ze specyficznej dla danej rodziny
ramy oraz specyfikacji funkcjonalności. Rama jest programem posiadającym
interfejs użytkownika (specyficzny dla danego obszaru zastosowań), mechanizmy
(m.in. analizator leksykalny i składniowy) do interpretacji specyfikacji oraz
mechanizmy do realizacji specyfikacji. Zaletą takiego podejścia jest duża możliwość
wpływania na działanie programu po jego wytworzeniu lub nawet dostarczeniu użytkownikowi.
Znajomość języków formalnych może wydatnie pomóc przy projektowaniu własnych
języków dla różnych produktów. Oczywiście podejście takie ma pewne wady
– interpretacja specyfikacji powoduje pewien nakład czasowy – można
temu częściowo zaradzić poprzez przekształcenie owej specyfikacji do pewnej
formy pośredniej. Jest to istotne również wtedy, gdy firmie wytwarzającej
oprogramowanie zależy na poufności. Oczywiście budowanie oprogramowania w
sposób przed chwilą opisany jest ewidentnie czym innym niż dodawanie do
programu nowych modułów, które mają taką czy inną funkcjonalność –
oba rozwiązania mogą iść jednak w parze. Do systemu (rama + specyfikacja) można
dodawać zarówno nowe fragmenty (jednostki specyfikacji) jak i środki służące
do jej realizacji czyli nowe moduły (jednostki realizacji), co przedstawiono na
rysunku 2.


Rys. 2. Rama, jednostki specyfikacji i realizacji

Na tym poziomie rozważań nie ma większego znaczenia postać
obu rodzajów jednostek. Jak już powiedziano jednostki specyfikacji mogą być
„skompilowane” lub też przedstawione w postaci czytelnej dla człowieka.
Ważne jest to, że specyfikację w nich zawartą zapisuje się przy pomocy
pewnego rodzaju języka, który jest specyficzny dla danej rodziny systemów.
Jednostki realizacji mogą być dostarczane jako obiekty COM, klasy Java,
biblioteki DLL itd. Oczywiście aktualnie istniejące (w systemie) jednostki
realizacji muszą być wystarczające do wykonania specyfikacji. Można założyć
(nie jest to jednak bezwzględnie konieczne), iż jedna jednostka specyfikacji
ma odpowiadającą sobie jednostkę realizacji.

IFAD VDM-SL

Język specyfikacji (i projektowania) VDM-SL jest formalnym
(wg autora półformalnym), nieobiektowym językiem ogólnego przeznaczenia.
Doczekał się on standardu ISO z tym, że jako przykład zostanie omówiony
dialekt firmy IFAD – IFAD VDM-SL, który stanowi pewne rozszerzenie
standardu języka. Różni się on od standardu m.in. obecnością modułów, co
umożliwia lepszy zapis specyfikacji. W obrębie języka można wyróżnić:

  • definicje typów,
  • definicje stanu,
  • wyrażenia,
  • instrukcje,
  • definicje funkcji i operacji.

Definicje typów – VDM posiada zarówno wbudowane typy
danych jak również możliwość definiowania typów danych użytkownika. Dla
typu można zdefiniować niezmiennik , który pozwala określić jakie wartości
są dozwolone dla zmiennych.

Definicje stanu – pozwalają na definiowanie
zmiennych globalnych z tym, że w standardzie ISO może występować tylko jedna
taka definicja w obrębie całej specyfikacji. W dialekcie IFAD zmienne globalne
można definiować w obrębie każdego modułu. Przykład definicji stanu
zostanie podany w dalszej części artykułu.

Instrukcje – W omawianym języku istnieją m.in.
instrukcje przypisania, warunkowe (if then else oraz case), iteracyjne, (for,
while itp) czyli spełnione są warunki niezbędne aby zapisać każdy algorytm.
Instrukcje mogą występować w operacjach. Przykładowa pętla for, w której
jest wykonywana pewna czynność dla każdego elementu ciągu c wygląda
następująco:

for e in s do
  s1:=s1^[e];

Trzeba jednak pamiętać, że zastosowanie instrukcji zbliża
specyfikację do pseudokodu.

Wyrażenia – występują m.in. wyrażenia:
warunkowe (if then else), wyrażenia lokalnej definicji (let), wyrażenia
unarne (unary -, not, card, len, hd, tail itp – niektóre z nich zostały
omówione przy opisywaniu przykładowych typów w tabeli 2), binarne (np.
dodawanie, odejmowanie liczb, suma mnogościowa zbiorów itp.), wyliczenie
elementów zbioru, wyliczenie elementów ciągu. Można przyjąć, iż spora część
wyrażeń jest dość podobna do znanych z języków programowania. Na uwagę
zasługuje fakt, że w omawianym języku istnieje zarówno instrukcja warunkowa
jak i wyrażenie warunkowe.

Definicje funkcji i operacji – W dokumentacji języka
VDM-SL napisano, iż służą one do definiowania algorytmów. Nie jest to
jednak, zdaniem autora, sformułowanie zbyt szczęśliwe, ponieważ algorytm
jest opisem czynności, które należy wykonać aby uzyskać określony rezultat
np. posortować ciąg liczb. W omawianym języku (w standardzie ISO także)
funkcje oraz operacje mogą być definiowane poprzez algorytm (explicite) lub właściwości
rozwiązania (implicite). Zauważmy, iż można to odnieść odpowiednio do języków
programowania imperatywnych i nieimperatywnych. Np. w języku C zapisujemy
algorytm opisujący jak otrzymać rozwiązanie, natomiast w języku SQL
opisujemy właściwości rozwiązania nie troszcząc się o to (pomijając fakt,
iż sposób zapisu może wpływać na efektywność wykonania), jak motor bazy
danych zrealizuje zapytanie. Zapis implicite bardziej odpowiada analizie i
modelowaniu, kiedy bardziej istotne jest co system robi, a nie sposób uzyskania
rozwiązania. (Dla definicji explicite możliwe jest określenie, że ciało
funkcji nie zostało jeszcze zapisane). Wykonanie funkcji nie wiąże się z żadnymi
dodatkowymi efektami, czyli nie można używać zmiennych globalnych. Użycie
tych ostatnich jest możliwe w operacjach. Poniżej przedstawiono bardzo prostą
definicję funkcji, która odwraca ciąg liczb.

functions
Odwroc : (seq of int) -> (seq of int)
Odwroc(s)==
        if len s = 0 then s
        else Odwroc(tl s) ^ [hd s];

Rozpoczyna się ona od sygnatury określającej typy argumentów
i typ wartości zwracanej – dla powyższego przykładu są to ciągi znaków.
Pod sygnaturą znajduje się definicja explicite. Działanie funkcji jest następujące:
jeśli ciąg jest pusty (wyrażenie len s ma wartość równą długości
ciągu s) to jest on zwracany jako wartość funkcji. W przeciwnym
wypadku dla ogona ciągu s wywoływana jest rekurencyjnie funkcja Odwroc
(tl s – „ogon” niepustego ciągu s). Następnie wykonywana
jest konkatenacja odwróconego ogona (hd s – pierwszy element niepustego
ciągu s) z pierwszym elementem ciągu (^ – konkatenacja ciągów).

Narzędzie The IFAD VDM-SL toolbox

Zanim zostanie omówiony bardziej konkretny przykład podamy
niezbędne informacje dotyczące pracy z narzędziem The IFAD VDM-SL toolbox.
Pozwala ono na sprawdzenie poprawności składniowej specyfikacji, sprawdzenie
zgodności typów, uruchamianie i debagowanie specyfikacji, oraz na wykonywanie
testów dla przygotowanych danych. Umożliwia ono również generowanie kodu źródłowego
w języku C++. Debuger, chociaż pozwala na wstawianie punktów przerwania, jest
uboższy niż te znane z popularnych środowisk programistycznych. Również samą
specyfikację przygotowuje się w zewnętrznym edytorze. Można ją zapisywać w
postaci tekstu ASCII, LaTeX oraz jako pliki formatu Reach Text Format (*.rtf). W
dokumentacji podano, że pliki w tym formacie należy przygotowywać w programie
MS Word, praktyka pokazuje, że można to robić np. edytorem Writer z pakietu
OpenOffice. Zastosowanie formatu rtf jest bardzo wygodne, ponieważ nie trzeba
rozdzielać specyfikacji na jej część zapisaną w języku naturalnym i
formalną, zapisaną w VDM. Obie części mogą być zapisane w jednym pliku, a
narzędzie (The IFAD VDM-SL Toolbox) czyta tylko akapity zapisane w stylu VDM.
(Jako ciekawostkę można podać, iż autor sporządził w ten sposób
zaprezentowaną dalej definicję bardzo prostego modułu przychodni lekarskiej
wraz z komentarzami.) Łatwo zauważyć, że utrzymanie jednego pliku zawierającego
formalny opis wraz z komentarzem lub opisem słownym dla systemu, podsystemu lub
modułu sprzyja spójności specyfikacji.

Przykład specyfikacji w IFAD VDM-SL

Jako, że podział sytemu na moduły (lub ich odpowiedniki)
stanowi kluczowe zagadnienie w inżynierii oprogramowania, praktycznym przykładem
będzie bardzo prosty moduł. (Trzeba jednak pamiętać, iż standardowy VDM-SL
nie posiada niestety mechanizmów służących do modularyzacji systemu.) Moduł
musi posiadać unikalną nazwę w obrębie całej specyfikacji, posiada on część
interfejsową oraz definicyjną. Pierwsza opisuje, jakie byty są udostępniane
reszcie specyfikacji oraz z jakich bytów zewnętrznych się korzysta. W drugiej
opisuje się funkcjonalność modułu.

Wracając na chwilę do rozważań o samej specyfikacji, można
zapytać co stanowi o jej sile. Podział na moduły był przecież już w języku
Modula, a jeśli chodzi o bardziej popularne języki programowania, to występował
w Borland Pascalu oraz Adzie. Więc modularyzacja – choć bardzo wygodna a
nawet nieodzowna – w praktyce nie stanowi o tym, że dana metoda jest
formalna. Należy pamiętać, że pisząc specyfikację słowną jest się narażonym
na nieścisłości; przy programowaniu trzeba z kolei myśleć w kategoriach
konkretnych rozwiązań technicznych. W implementacji ważne jest, gdzie
przechowuje się pewne dane (w pliku, tablicy w bazie danych). Na poziomie
specyfikacji w języku VDM nie ma to znaczenia, ponieważ istnieje pojęcie
odwzorowania. Projektant (a przede wszystkim analityk) jest za to zmuszony
precyzyjnie opisać co system robi, jak działa model (ale nie system); nie musi
natomiast troszczyć się o rozwiązanie. Z punktu widzenia specyfikacji
(systemu nie języka!) tablica w języku programowania pozwala na odwzorowanie
indeksu na pewną wartość w niej przechowywaną. Jeśli chodzi o tabelę w
bazie danych, to odwzoruje się (mówiąc bardzo ogólnie) klucz na pewną wartość,
zatem są to przykłady pewnych odwzorowań. Oczywiście nie da się, w miarę
zbliżania się do implementacji, uniknąć decyzji jak „coś”
przechowywać.

Poniżej przedstawiono moduł Osoby, który służy do
przechowywania danych o osobach w systemie. Omawiany moduł eksportuje jeden typ
danych (Osoba) i trzy operacje:

  • Nowa_osoba
  • Usun_osoba
  • Pobierz_osoba

Pierwsza z nich dodaje nową osobę, druga usuwa a trzecia
pobiera dane osoby. Operacje te mogą być używane (pod warunkiem ich
zaimportowania) w pozostałych modułach. Formalnie – deklarując
eksporty, trzeba podać sygnatury funkcji, czyli typy argumentów i typ wartości
zwracanej. Bardziej interesująca z punktu widzenia zastosowania metod
formalnych jest część definicyjna modułu. W przykładowym module rozpoczyna
się ona od definicji typów – pierwsza z nich znajduje się poniżej:

cyfra = nat
inv c == c<10;

Nowo definiowany typ cyfra jest podtypem wbudowanego
typu nat, który odpowiada liczbom naturalnym. Niezmiennikiem (ang.
invariant) tego typu jest to, że zmienna tego typu musi mieć wartość mniejszą
od 10 (c to przykładowa zmienna tego typu). Tak więc nowo
wprowadzony typ reprezentuje cyfry od 0..9.

Mechanizm niezmienników pozwala na zdefiniowanie pewnych
warunków, jakie muszą spełniać zmienne lub pola w rekordzie. Dalej
zdefiniowano typy, użyte później przy definicji typu rekordu osoba.
Typ Timie jest niepustym ciągiem znaków, z kolei typ Tpesel jest
ciągiem (zdefiniowanych poprzednio) cyfr o długości 10. Osoba jest rekordem,
którego pola wynikają wprost z opisu rzeczywistości przychodni lekarskiej.
Dalej znajduje się definicja stanu czyli zmiennych globalnych modułu i
definicja operacji.

Specyfikacja przychodni lekarskiej – Moduł Osoby

module Osoby

Poniżej określamy typy i operacje (w ogólności również
funkcje), które będą widoczne dla pozostałej części specyfikacji.

exports
    types
        Osoba;
    operations
        Nowa_osoba : Tid_osoba * Osoba ==> ();
        Usun_osoba : Tid_osoba ==> ();
        Pobierz_osoba : Tid_osoba ==> Osoba;

Tutaj rozpoczyna się część definicyjna modułu: w
pierwszej jej części określamy typy, następnie zmienne globalne tego modułu
oraz kilka przykładowych operacji.

definitions
types
    cyfra = nat
    inv c == c<10;
    Timie = seq1 of char;
    Tnazwisko = seq1 of char;
    TNIP = seq1 of cyfra;
    TPESEL = seq1 of cyfra
    inv pesel == len pesel = 10;
    Ttelefon = seq1 of cyfra;
    Tadres = seq1 of char;
    Tid_osoba = seq1 of char;

Osoba :: imie : Timie
    nazwisko : Tnazwisko
    NIP : TNIP
    PESEL : TPESEL
    telefon : Ttelefon
    telfon_kom : Ttelefon
    adres : Tadres;

Definicja zmiennych globalnych:

    state osoby_w_przychodni of
        osoby : map Tid_osoba to Osoba

    end
operations

Poniższa definicja składa się z sygnatury (iloczyn
kartezjański typów argumentów oraz typ zwracany) i wyrażenia, opisującego,
co operacja robi.

    Czy_mozna_dodac : Tid_osoba ==> bool
    Czy_mozna_dodac(id)==
        return not id in set dom osoby;

    Nowa_osoba : Tid_osoba * Osoba ==> ()
    Nowa_osoba(id, o) ==
        osoby := osoby munion {id |-> o}
    pre Czy_mozna_dodac(id);

    Usun_osoba : Tid_osoba ==> ()
    Usun_osoba(id)==
        osoby := {id} <-: osoby
    pre id in set dom osoby;

    Pobierz_osoba : Tid_osoba ==> Osoba
    Pobierz_osoba(id) ==
        return osoby(id)
pre id in set dom osoby;
end Osoby

Generowanie kodu w C++ ze specyfikacji IFAD VDM-SL

Automatyczne generowanie kodu, w opini autora, ma miejsce
wtedy, gdy ze specyfikacji potrafimy uzyskać algorytm zapisany w języku
programowania. Przy tak przyjętej definicji nie jest automatycznym generowaniem
kodu wytworzenie definicji klasy i szkieletów metod, które należy ręcznie
uzupełnić kodem.

Narzędzie firmy IFAD pozwala generować ze specyfikacji kod
źródłowy C++. Dla przedstawionej wcześniej funkcji odwracającej ciąg znaków
zostały wygenerowane cztery pliki:

  • DefaultMod.cpp,
  • DefaultMod.h
  • DefaultAnonym.cpp,
  • DefaultAnonym.h.

Poniżej zaprezentowano te pliki (usunięto z nich, dla
zaoszczędzenia miejsca, informacje o tym że zostały wygenerowane
automatycznie przez narzędzie VDM-SL to C++ Code Generator itp.). Już na
pierwszy rzut oka widać, że z zajmującej cztery linie funkcji powstało ponad
pięćdziesiąt linii kodu.

#include "DefaultMod.h"

void init_DefaultMod_VDMLib () {
VDMGetDefaultRecInfoMap().NewTag
(TOKEN, 1);
    VDMGetDefaultRecInfoMap().SetSymTag(TOKEN, "token");
}

#ifdef DEF_DefaultMod_USERIMPL
#include "DefaultMod_userimpl.cpp"
#endif

void init_DefaultMod () { init_DefaultMod_VDMLib();
}

#ifndef DEF_DefaultMod_Odwroc

type_iL vdm_DefaultMod_Odwroc (const type_iL &vdm_DefaultMod_s) {
Sequence varRes_3;

    if (((Bool) ((Int) vdm_DefaultMod_s.Length() == (Int)
0)).GetValue())
        varRes_3 = vdm_DefaultMod_s;
    else { Sequence var2_12;

        var2_12 =
Sequence().ImpAppend((Int) vdm_DefaultMod_s.Hd());
       
varRes_3.ImpConc(vdm_DefaultMod_Odwroc((Generic) vdm_DefaultMod_s.Tl())).ImpConc(var2_12);

    }
    return (Generic) varRes_3;

}
#endif

DefaultMode.cpp

#ifndef _DefaultMod_h
#define _DefaultMod_h
#include <math.h>
#include "metaiv.h"
#include "cg.h"
#include "cg_aux.h"
#include "DefaultMod_anonym.h"
void init_DefaultMod ();
type_iL vdm_DefaultMod_Odwroc (const type_iL &);
#endif

DefaultMode.h

#ifndef _DefaultMod_anonym_h
#define _DefaultMod_anonym_h
#include "DefaultMod_userdef.h"
#include "metaiv.h"
class type_iL;
#ifndef TAG_type_iL
#define TAG_type_iL (TAG_DefaultMod + 1)
#endif

#ifndef DECL_type_iL
#define DECL_type_iL 1

class type_iL : public SEQ<Int> {
public:
    type_iL () : SEQ<Int>() {}
    type_iL (const SEQ<Int> &c) : SEQ<Int>(c) {}
    type_iL (const Generic &c) : SEQ<Int>(c) {}
    const char * GetTypeName () const {
    return "type_iL";
    }

} ;
#endif
#endif

DefaultMod_anonym.h

#include "DefaultMod_userdef.h"
#include "metaiv.h"
#include "DefaultMod.h"

DefaultMod_anonym.cpp

W pliku DefaultMode_anonym.h zdefiniowany został nowy typ
type_iL, który powstał poprzez parametryzację wzorca SEQ typem int. Ten
– pierwszy jak łatwo się domyślić (nie ma go w wygenerowanym kodzie)
definiuje ciąg ogólnego przeznaczenia. Na marginesie tych rozważań można
zauważyć, że zdefiniowano tylko konstruktory – jest to zrozumiałe
dlatego, że muszą mieć one nazwe zgodną z nazwą klasy. Sama funkcja
odwracająca zdefiniowana jest w pliku DefaultMode.cpp, w którym występuje
pod nazwą vdm_DefaultMod_Odwroc. Ciąg DefaultMod jest nazwą modułu, w którym
umieszczono definicję funkcji; jeśli funkcja nie została zdefiniowana w obrębie
modułu, to przyjmuje się domyślną nazwę modułu DefaultMod. Warto przyjrzeć
się wygenerowanej automatycznie funkcji raz jeszcze:

type_iL vdm_DefaultMod_Odwroc (const type_iL &vdm_DefaultMod_s)
{
    Sequence varRes_3;
    if (((Bool) ((Int) vdm_DefaultMod_s.Length() == (Int) 0)).GetValue())
        varRes_3 = vdm_DefaultMod_s;
    else { Sequence var2_12;
        var2_12 = Sequence().ImpAppend((Int)
vdm_DefaultMod_s.Hd());
        varRes_3.ImpConc(vdm_DefaultMod_Odwroc((Generic)
vdm_DefaultMod_s.Tl())).ImpConc(var2_12);
    }
return (Generic) varRes_3;
}

W zasadzie tłumaczenie ze specyfikacji VDM-SL na C++ polega
(w tym przykładzie!) na zamianie wywołań operatorów dla ciągów takich jak
hd, tl, w VDM na wywołania odpowiadających im metod klasy type_iL, która
reprezentuje ciąg liczb typu integer. Należy zwrócić uwagę, iż tak
uzyskany kod źródłowy zależy bardzo silnie od bibliotek, które definiują
odpowiadające typom wbudowanym klasy. Poprawność programu zależy zatem nie
tylko od poprawności samej specyfikacji ale też od tych bibliotek. Trudno się
oprzeć wrażeniu, że kod napisany ręcznie byłby bardziej czytelny.
Specyfikacja funkcji jest rekurencyjna, co czyni ją czytelną. Nie oznacza to,
że również implementacja musi być realizowana w ten sposób – tym
bardziej, że znane są algorytmy derekursywacji. Człowiek z pewnością napisał
by taką funkcję iteracyjnie. Należy zauważyć, że trudno przewidzieć długość
ciągów które będą odwracane. Dla niewielkich długości nie ma żadnego
problemu. Pojawi się on jednak dla długich ciągów – może bowiem nastąpić
przepełnienie stosu na skutek dużej ilości wywołań rekurencyjnych. Jest to,
jak się wydaje, problem dość ogólny polegający na ograniczeniach
implementacyjnych. Oczywiście w języku VDM-SL możliwe jest zdefiniowanie
operacji, która robi to samo w sposób iteracyjny.

Poniżej zdefiniowano taką właśnie operacje (w funkcji nie
można używać instrukcji tylko wyrażenia).

operations
Odwroc : (seq of int) ==> (seq of int)
Odwroc(s)==
    (dcl s1 : seq of int := [];
    for e in reverse s do
   

s1:=s1^[e];

    return s1;
    )

Wyrażenie dcl s1 : seq of int := []; wprowadza nową
zmienną, która jest ciągiem liczb int.

Pętla for przechodzi od tyłu przez wszystkie
elementy ciągu s. W pogrubionym wyrażeniu na koniec ciągu s1 dołączane
są kolejne elementy z ciągu s. Tym razem została wygenerowana
iteracyjna wersja funkcji:

type_iL vdm_DefaultMod_Odwroc (const type_iL &vdm_DefaultMod_s) {
Sequence vdm_DefaultMod_s1 = Sequence();
{
    Int vdm_DefaultMod_e;
    for (int i_11 = vdm_DefaultMod_s.Length();
    i_11 > 0; i_11—) { Int elem_5 = vdm_DefaultMod_s[i_11];

    vdm_DefaultMod_e = elem_5;
    vdm_DefaultMod_s1.ImpAppend(vdm_DefaultMod_e);
    }
}
return (Generic) vdm_DefaultMod_s1;
}

The IFAD VDM++

Język ten służy do tworzenia obiektowych specyfikacji i
stanowi rozszerzenie języka IFAD VDM-SL. Posiada on też mechanizmy służące
do modelowania współbieżności. Wprowadzono w nim pojęcie klasy analogiczne
do tego, które występuje w językach programowania. W obrębie klasy można
definiować typy, zmienne instancji, funkcje oraz operacje. Poniżej
zaprezentowano przykład klasy, która odpowiada zaprezentowanemu wcześniej
modułowi (wprowadzono pewne uproszczenia, aby wygenerowany automatycznie kod był
jak najkrótszy). Klasa taka nie powinna jednak istnieć w rzeczywistym
projekcie. W obrębie klasy można definiować typy. W poniższym przykładzie różnią
się od prezentowanych poprzednio wyłącznie określeniem widoczności. To samo
dotyczy definicji funkcji i operacji.

class OsobyDB
types
    public Timie = seq1 of char;
    public Tnazwisko = seq1 of char;
    public Tid_osoba = seq1 of char;
    public Osoba :: imie : Timie
        nazwisko : Tnazwisko

    instance variables
        osoby : map Tid_osoba to Osoba
operations
    private Czy_mozna_dodac : Tid_osoba ==> bool
    Czy_mozna_dodac(id)==
        return not id in set dom osoby;

    public Nowa_osoba : Tid_osoba * Osoba ==> ()
    Nowa_osoba(id, o) ==
        osoby := osoby munion {id |-> o}
    pre Czy_mozna_dodac(id);

    public Pobierz_osoba : Tid_osoba ==> Osoba
    Pobierz_osoba(id) ==
        return osoby(id)
    pre id in set dom osoby;
end OsobyDB

Generowanie kodu źródłowego w języku Java ze specyfikacji w VDM++

Poniżej zaprezentowano (nieznacznie zmieniony) automatycznie
generowany z powyższej specyfikacji kod w języku Java. Narzędzie pozwala również
na generowanie kodu w języku C++. Poprawki wprowadzone początkowo przez autora
polegały na usunięciu pewnych komentarzy (jakim narzędziem wygenerowano itp.)
oraz przeformatowaniu kodu tak, aby zajmował jak najmniej miejsca. Niestety nie
dało się stworzyć obiektu klasy osoba, ponieważ wewnętrzna klasa
Osoba była statyczna. Trzeba było ręcznie poprawić kod, używając
specyfikator static dla omawianej klasy. Kod jest dość obszerny i korzysta z
pakietów dostarczonych przez firmę IFAD. Warto przyjrzeć się bliżej, jak
realizowane jest tłumaczenie. Ciągi znaków są reprezentowane w Javie jako
obiekty klasy String. Natomiast ciągi cyfr (zostały one dla oszczędności
miejsca usunięte z prezentowanego poniżej kodu) tłumaczone były na obiekty
klasy Vector. To samo miało miejsce, gdy wyprowadzono nowy typ z char. Nawet
przy pisaniu funkcji testowej okazało się to bardzo niezręczne, ponieważ aby
zdefiniować numer telefonu należało stworzyć nowy obiekt klasy Vector i dodać
do niego po kolei kolejne cyfry owego numeru.

Nie ulega wątpliwości, iż człowiek nie napisał by kodu w
ten sposób. Oczywiście tłumaczenie takie jest poprawne w przypadku kiedy nie
założy się pewnej maksymalnej długości numeru telefonu. Człowiek się domyśli
– generator nie. O problemie można mówić wtedy, gdy określi się
maksymalną długość numeru telefonu lub długość NIP-u, a w kodzie
otrzymuje się nadal wektor. Bardziej wygodne jest zastosowanie w specyfikacji
ciągu znaków i zrezygnowanie w ogóle z ograniczania podzbioru znaków –
generator użyje wtedy obiektów klasy String. Można jednak zapytać, czy nie
jest to aby sytuacja trochę patologiczna? Albo godzimy się na otrzymanie
niewygodnego w użyciu kodu, albo trzeba naginać specyfikację. Odwzorowanie
jest tłumaczone na klasę HashMap, która opowiada tablicy haszującej. Warto
dodać, że w opcjach generowania kodu dla języka Java można ustawić np., czy
mają być używane konstrukcje współbieżne.

import dk.ifad.toolbox.VDM.*;
import java.util.*;

public class OsobyDB {

  public class Osoba implements Record {

    public String imie;
    public String nazwisko;

    public Osoba () {}
    public Osoba (String p1, String p2) {
        imie = p1;
        nazwisko = p2;
    }
    public Object clone () {
        return new Osoba(imie,nazwisko);
    }
    public String toString () {
    return "mk_OsobyDB`Osoba(" + UTIL.toString(imie) +
"," + UTIL.toString(nazwisko) + ")";
    }
    public boolean equals (Object obj) {
        if (!(obj instanceof Osoba))
            return false;
        else {
            Osoba temp = (Osoba)
obj;
            return UTIL.equals(imie, temp.imie) &&
UTIL.equals(nazwisko, temp.nazwisko);
        }
    }
    public int hashCode () {
        return (imie == null ? 0 : imie.hashCode()) + (nazwisko == null ? 0 :
nazwisko.hashCode());
        }

    };
static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
    private HashMap osoby = new HashMap();
    private Boolean Czy_umozna_udodac (final String id) throws    
CGException{
    Boolean rexpr_3 = null;
    Boolean unArg_4 = null;
    TreeSet var2_6 = new TreeSet(vdmComp);
    var2_6.clear();
    var2_6.addAll(osoby.keySet());
    unArg_4 = new Boolean(var2_6.contains(id));
    rexpr_3 = new Boolean(!unArg_4.booleanValue());
    return rexpr_3;
}

public void Nowa_uosoba (final String id, final Osoba o) throws CGException{
    HashMap rhs_4 = new HashMap();
        HashMap var2_6 = new HashMap();
    var2_6 = new HashMap();
    var2_6.put(id, o);
{
    HashMap m1_13 = (HashMap) osoby.clone();
    HashMap m2_14 = var2_6;
    TreeSet com_9 = new TreeSet(vdmComp);
        com_9.addAll(m1_13.keySet());
    com_9.retainAll(m2_14.keySet());
    boolean all_applies_10 = true;
    Object d_11;
    for (
        Iterator bb_12 = com_9.iterator();
            bb_12.hasNext() && all_applies_10; ) {
        d_11 = bb_12.next();
        all_applies_10 = m1_13.get(d_11).equals(m2_14.get(d_11));
    }
    if (!all_applies_10)
        UTIL.RunTime("Run-Time Error: Map Merge: Incompatible maps");
    m1_13.putAll(m2_14);
    rhs_4 = m1_13;
}
    osoby = (HashMap) UTIL.clone(rhs_4);
}

public Boolean pre_Nowa_uosoba (final String id, final Osoba o) throws
CGException{
    return (Boolean) Czy_umozna_udodac(id);
}
public Osoba Pobierz_uosoba (final String id) throws CGException{
    return (Osoba) osoby.get(id);
}

public Boolean pre_Pobierz_uosoba (final String id) throws CGException{
    Boolean varRes_3 = null;
    TreeSet var2_5 = new TreeSet(vdmComp);
    var2_5.clear();
    var2_5.addAll(osoby.keySet());
    varRes_3 = new Boolean(var2_5.contains(id));
    return varRes_3;
    }
};

Prosty program testujący powyższy kod wygląda następująco:

import java.util.Vector;
public class Main{
public static void main(String args[]){
OsobyDB osoby = new OsobyDB();
try{
    osoby.Nowa_uosoba("1", osoby.new
Osoba("Jan","Kowalski"));
    osoby.Nowa_uosoba("2", osoby.new
Osoba("Bo","Johns"));
    osoby.Nowa_uosoba("3", osoby.new Osoba("Paweł","Iksiński"));
}catch(dk.ifad.toolbox.VDM.CGException cge){
    cge.printStackTrace();
}
try{
    OsobyDB.Osoba o = osoby.Pobierz_uosoba("3");
    System.out.println(o.imie+" "+o.nazwisko);
}catch(dk.ifad.toolbox.VDM.CGException cge){
    cge.printStackTrace();
}
}

Podsumowując należy stwierdzić, iż języki IFAD VDM-SL
oraz IFAD VDM++ są mocnymi narzędziami w zakresie definiowania specyfikacji
systemu. Można natomiast mieć duże zastrzeżenia jeśli chodzi o kod
generowany przez generatory kodu. Dotyczy to zarówno generatora C++ (VDM-SL)
jak i Java (VDM++). Zdaniem autora, omawiane narzędzia (i języki) bardziej
nadają się do modelowania systemu, niż do jego projektowania. Mogą one być
jednak bardzo przydatne do projektowania pewnych, newralgicznych fragmentów
systemu. Znajomość metod formalnych może być również wykorzystana przy
projektowaniu oprogramowania opartym o koncepcje rodzin lub
o metodę zaproponowaną przez autora.

Cdn.

Literatura

[1] Formal Methods and Verification Guidebook for Software and Computer Systems Vol. I Planning and Technology Insertion, NASA 1998
[2] Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems Vol. II A Practitioner’s Companion
[3] The IFAD VDM-SL Language, IFAD 1999
[4] VDM-SL Toolbox User Manual, IFAD 2000
[5] The IFAD VDM++ Language, IFAD 2000
[6] The VDM++ to Java Code Generator, IFAD 2000