Typy danych

Formalna specyfikacja i analiza typów danych zajmuje ważną pozycję we współczesnych badaniach związanych z semantyką języków programowania i procesem weryfikacji programów.

Zastanówmy się przez chwilę czym są typy danych. Przede wszystkim zauważmy, że typu danych nie określa jedynie zbiór wartości, jakie mogą być przyjmowane przez zmienne tego typu. Na przykład inne własności ma zbiór liczb naturalnych rozpatrywany jedynie z działaniem dodawania, a inne ten sam zbiór z działaniem mnożenia (różnice są tu o wiele głębsze niż się to może wydawać na pierwszy rzut oka - np. zbiór formuł (z dodawaniem) prawdziwych w zbiorze liczb naturalnych jest rozstrzygalny podczas gdy mnożenie powoduje iż staje się on nierozstrzygalny nawet częściowo). Podobnie, para liczb rzeczywistych może określać liczbę zespoloną (jeśli odpowiednio określimy działania dodawania i mnożenia), natężenie i napięcie prądu w przewodniku (jeśli określimy np. operację obliczania oporu przewodnika). Typ stosy różni cd typu kolejki jedynie definicja operacji wstawiania elementu (na początek‘stosu, na koniec kolejki), podczas gdy same wartości tych typów (skończone ciągi elementów) nie różnią się od siebie. Tak więc dane różnych typów są rozróżnialne nie tylko przez ich wartości, lecz takie przez operaq'e z nim związane. Odpowiednim formalizmem do modelowania (nie specyfikowania!) typów danych będą więc systemy relacyjne mające właśnie ich (typów) strukturę.

4.1 Przykład: Arytmetykę liczb naturalnych definiujemy jako system relacyjny ł ł = <N;0,1,+ > , gdzie każdy elment N jest albo zerem, albo powstaje w wyniku

dodania do zera skończonej (!) liczby jedynek, zaś mają standardowe znaczenie.//

4-2 Przykład: Załóżmy, że mamy dany pewien typ E, o którym zakładamy jedynie, iż zdefiniowano w nim wyróżnioną stalą (funkcję zeroargumentową) ERROR oraz relację =^e porównywania wartości (typu E). Stosy elementów typu E definiujemy jako system relacyjny (dwusortowy) < E,S;ERROR,top,push,pop,empty,*=E, = S>,gdzie:

4.3 Przykład: Typ drzew binarnych (każdy wierzchołek ma co najwyżej dwóch synów) definiujemy jako system relacyjny < D;left,right,cons,empty > , gdzie:

(i) D jest zbiorem wszystkich skończonych (!) wyrażeń (termów) żawierającym empty (drzewo puste) i spełniającym warunek, że jeśli do Dnależą di i d², to należy także wyrażenie cons(di,d?) (drzewo, którego lewym poddrzewem jest di, a prawym - d2);

(ii) left(cmjłD;) = right(empiy) = cmpiy; łcfi(cQjQs(di,d2)) = dr, right(cmis(di,d2)) = d2; (iii) cons(di,d2) = cons(di,d2); empty = empty.

Dla odróżnienia elementów zbioru D od funkcji, nazwy tych pierwszych podkreśliliśmy.//

Podobne semantyczne definicje typów danych są wysoce niewygodne w procesie dowodzenia własności programów, nie są bowiem opisane w kategoriach pozostających na wystarczającym poziomie abstrakcji i przystających do metod wnioskowania omawianych w trzecim rozdziale. Skrajnym przykładem definicji tego typu byłoby wyznaczenie semantyki języka programowania poprzez działanie kompilatora. Dążymy zatem zawsze do zdefiniowania semantyki typu danych poprzez podanie najbardziej podstawowych własności danych i operacji w nim występujących. W zależności od siły przyjętej logiki i podanych w niej własności możemy uzyskać lepszy łub gorszy opis interesującego nas typu danych.

Logiczna specyfikacja typu danych składać się będzie zatem tylko z najważniejszych informacji o typie, bez wnikania w sposób jego implementacji. Do informacji tych należy po pierwsze sygnatura operacji (inaczej ich składnia, określająca dziedziny i przeciwdziedziny) w definicjach semantycznych występująca pośrednio, a po drogie zestaw aksjomatów precyzujących własności danych i operaqi. Abstrahując od konkretnej implementacji (innymi słowy - od konkretnej semantycznej definicji typu danych) musimy znów zwrócić uwagę na problemy analogiczne do poprawności i pełności systemów wnioskowania. Odpowiednikiem poprawności jest w przypadku typu danych zapewnienie, iż specyfikacja ma jakąkolwiek implementaq’ę (istnieje dla mej model).Mówimy wówczas o niesprzeczności specyfikacji.

Odpowiednikiem pełności jest zapewnienie, że specyfikacja umożliwi dowodzenie rozsądnego zbioru własności, czyli zawiera w sobie odpowiedź na rozsądny zbiór pytań jakie może postawić programista implementujący typ danych (mówimy wówczas o zupełności).

4.4 Definicja: Powiemy, że specyfikacja typu danych, której aksjomaty wyrażone zostały zbiorem Z formuł logiki L = < F.l^Sa/ > , jest niesprzeczna wttw, gdy Z ma model (istnieje interpretaq'a 1 taka, że I Sal Z). Powiemy, że specyfikacja ta jest zupełna, jeśli każda formuła

bez zmiennych wolnych, bądi jej zaprzeczenie jest konsekwenq'ą (semantyczną) zbioru Z.//

21auważmy, iż specyfikacje budujemy, mając w głowie pewien model i dbając o to, aby wyrażane własności ten właśnie model opisywały. Przy poprawnym (zgodnym z zamierzeniami) wyrażaniu własności niesprzeczność uzyskujemy zatem praktycznie "za darmo" (za błędy tu popełnione trzeba jednak słono płacić!). Uzyskanie zupełnych specyfikacji jest problemem znacznie trudniejszym, często niemożliwym do rozwiązania. W literaturze rozważane są także inne, słabsze (a więc łatwiejsze do uzyskania) pojęcia zupełności, np. tzw. wystarczająca zupełność rozważana w kontekście badań informatycznych przez Guttaga (por. np. [Tur’82]), a będąca adaptacją pojęcia słabej reprezentowalności, znanego z logiki klasycznej (por. np.

[Grz’75]). Zakłada się tu, że wystarczającą dla programisty wiedzą jest możliwość wykazania dla każdej operacji f typu danych wszystkich prawdziwych twierdzeń postaci f(ci cn) = d, gdzie cj,...,cn,d są termami stałymi (nie zawierającymi zmiennych). Podkreślmy w tym miejscu, iż kryterium wystarczającej zupełności stanowi program minimum (wynikający ze słabości klasycznej logiki Li - o czym za chwilę), bowiem w procesie dowodzenia własności programów często niezbędna jest istotnie szersza wiedza niż oferowana przez specyfikacje "wystarczająco zupełne".

4.5 Przykład: Sygnatura typu danych liczb naturalnych (4.1) jest następująca:

0,1: - > N ; + ,* :N x N -> N ; < , = : N x N - > {true,false}.

Jako aksjomaty specyfikacji tego typu przyjąć można np. zestaw aksjomatów Peano, wyrażonych w języku logiki pierwszego rzędu:

Powyższy zbiór aksjomatów (schematy aksjomatów traktować będziemy, jak zwykle, jako nieskończone zbiory aksjomatów powstałe przez podstawienie konkretnych formuł w miejsce

Powyższy przykład wskazuje na pewne poważne ograniczenie klasycznej logiki pierwszego rzędu w możliwości specyfikowania typów danych. Można pokazać także następujące fakty dotyczące tej logiki:

- każda specyfikacja ma modele niestandardowe (różne od zamierzonych) - por. tw. Skolema, Lowenheima, Tarskiego np. w [Grz’75];

- nie można wyrazić ani skończoności elementów typu danych (liczb naturalnych, stosów, drzew itd.) - por. np. [MS’87], ani skończoności jego dziedziny - por. tw. Trakhtenbrota, np. w [EFT84];

- istnieją typy danych o tej własności, że można wykazać wszystkie twierdzenia postaci A(c), gdzie c jest dowolnym elementem dziedziny (stałą), zaś nie da się wykazać twierdzenia ogólnego (Vx)(A(x)) - por. np. [Grz’75].

Jak pokażemy dalej, ograniczenia te nie dotyczą logik silniejszych niż Li.