Uniwersytet Warszawski
Wydział Matematyki, Informatyki i Mechaniki

Praca magisterska napisana w Instytucie Informatyki

Weryfikacja poprawności projektów implementacji
modułów programistycznych

autor: Grzegorz Marczyński; Nr albumu: 153316; Promotor: dr Janina Mincer-Daszkiewicz

Warszawa, wrzesień 1999


 
Spis Treści

1 Wstęp

2 Metoda tropów

2.1 Założenia
2.2 Projekt interfejsu modułu
2.3 Projekt implementacji modułu
2.4 Przejście od projektu implementacji do konkretnego języka programowania

3 Metoda tropów w PVS

3.1 Wprowadzenie
3.2 Zanurzenie projektu interfejsu modułu w PVS
3.2.1 Trop jako skończona sekwencja
3.3 Sekcje składające się na projekt implementacji
3.3.1 Opis modułu
3.3.2 Struktury danych
3.3.3 Funkcja abstrakcji
3.3.4 Funkcje programu
3.3.5 Przydzielanie i zwalnianie obiektów
3.4 Obligacje poprawności projektu implementacji
3.4.1 Postać obligacji
 3.5 Kategorie projektów implementacji
3.6 Uwagi dotyczące nazewnictwa plików i teorii

4 Przykłady projektów implementacji

4.1 Teorie i struktury danych używane w przykładach
4.2 Wielomodułowe projekty implementacji
4.2.1 Wstęp
4.2.2 Specyfikacja modułu kolekcji
4.3 Obligacje poprawności systemu zarządzania obiektami
4.4 Projekty implementacji pojedynczego obiektu
4.4.1 Przykład: stos jako skończona sekwencja
4.5 Zdecentralizowane projekty implementacji
4.5.1 Przykład: stos jako tablica po stronie klienta
4.5.2 Przykład: stos jako lista po stronie klienta
4.5.3 Przykład: zdecentralizowany projekt implementacji kolekcji
4.6 Scentralizowane projekty implementacji
4.6.1 Przykład: tablica stosów implementowanych jako tablice
4.6.2 Przykład: kolekcja stosów reprezentowanych przez tropy kanoniczne stosu
4.7 Mieszane projekty implementacji
4.7.1 Przykład: stos jako trop kanoniczny po stronie modułu i u klienta

5 Uwagi dotyczące obligacji i ich dowodzenia

5.1 Postać obligacji
5.1.1 Obligacje generowane automatycznie jako TCC
5.1.2 Obligacje, które nie generują się jako TCCs
5.2 Dowody obligacji
5.2.1 Kroki dowodowe specyficzne dla nowej postaci tropów
5.2.2 Funkcja abstrakcji jest dobrze zdefiniowana - (1a) i (1b)
5.2.3 Funkcja abstrakcji odwzorowuje wartości początkowe struktury danych na trop kanoniczny równoważny tropowi pustemu - (2)
5.2.4 Funkcje programów zachowują poprawność struktury danych - (3a) i (3b)
5.2.5 Istnienie kolejnego stanu - (4)
5.2.6 Diagram przejść na poziom projektu interfejsu poprzez funkcję af jest przechodni - (5)
5.2.7 Funkcje programu przekazują wartości obce odpowiadające opisowi na poziomie projektu interfejsu - (6)
5.2.8 Wszelkie parametry, dla których wywołanie programu dostępu jest dopuszczalne należą do dziedziny odpowiadającej mu LD-relacji - (7)
5.3 Dowody obligacji w projektach wielomodułowych
5.4 Zasadność stosowania obligacji

6 Wnioski

6.1 Spostrzeżone ograniczenia
6.1.1 Jak wyrazić połączenie różnych implementacji tego samego interfejsu?
6.1.2 Jak wymusić zastosowanie projektu implementacji pojedynczego obiektu przy projektach wielomodułowych?
6.2 Nowy sposób podziału projektów implementacji
6.2.1 Dwa rodzaje projektów implementacji
6.3 Schematy konstrukcji wielomodułowych projektów implementacji
6.3.1 Schemat konstrukcji scentralizowanych projektów implementacji
6.3.2 Schemat konstrukcji mieszanych projektów implementacji
6.4 Etapy tworzenia projektów implementacji

7 Podsumowanie

Bibliografia