Next: Literatura Up: Specyfikacja wskaźnikowych struktur danych Previous: Zawartość pracy
Podsumowanie
Praca ta stanowi krok ku połączeniu metod formalnych specyfikacji oraz efektywnych algorytmów i struktur danych. Jej celem było pokazanie formalizmu pozwalającego na (względnie zwięzłe) specyfikowanie wskaźnikowych struktur danych i weryfikowanie programów względem specyfikacji zapisanych w tym formalizmie. Postawiony cel został osiągnięty -- logika wielościeżkowa oraz przedstawiony wariant logiki Hoare'a spełniają wymagania postawione w tezie.Nie wszystkie idee prezentowane w pracy są oryginalnym wkładem autora. Zaproponowana w pracy logika wielościeżkowa w dużej mierze opiera się na logice zaproponowanej przez Costę i Reggio w [CR97]. Przedstawiona wersja logiki Hoare'a powstała po przeanalizowaniu różnych wersji takich logik znanych z literatury. Dowody poprawności i pełności w sensie Cook'a prezentowanego systemu dowodzenia są wzorowane na standardowych dowodach tych własności zawartych w pracy [Apt81]. Do oryginalnych osiągnięć niniejszej rozprawy można zaliczyć ideę wykorzystania operatorów modalnych do opisu powiązań wskaźnikowych tworzących strukturę danych, analizę różnych formalizmów pod kątem ich przydatności do specyfikowania stosowanych wskaźnikowych struktur danych, a także wykorzystanie wszystkich tych idei przy opracowaniu logiki wielościeżkowej oraz prezentowanego wariantu logiki Hoare'a wraz z systemem dowodzenia.
Niestety musimy nadmienić, że przykład dowodu poprawności programu operującego na wskaźnikach przeprowadzony za pomocą prezentowanego formalizmu jest jeszcze bardziej skomplikowany niż ma to miejsce w przypadku klasycznej logiki Hoare'a i bezwskaźnikowych struktur danych. Stawia to pod znakiem zapytania jego praktyczną stosowalność. Problem ten dotyczy zresztą chyba wszystkich metod dowodzenia poprawności programów -- dowody są zbyt skomplikowane, aby je stosować w praktyce. Niezbędne wydają się zarówno opracowanie narzędzi wspomagających weryfikację oprogramowania, jak i praca nad dalszym uproszczeniem specyfikacji i weryfikacji programów.
Niniejsza praca nie wyczerpuje oczywiście poruszonej problematyki. Dalsze badania powinny się koncentrować na kilku tematach. Przede wszystkim należy zbadać na kolejnych przykładach praktyczną użyteczność propozycji zawartych w tej pracy i zastanowić się nad dalszą możliwością uproszczenia specyfikacji wskaźnikowych struktur danych i weryfikacji programów operujących na nich. Otwarty pozostaje problem weryfikacji specyfikacji wskaźnikowych struktur danych względem specyfikacji abstrakcyjnych typów danych. W ramach przyjętego przez nas podejścia funkcyjnego problem ten sprowadza się głównie do problemu definiowania funkcji abstrakcji dla wskaźnikowych struktur danych.
Next: Literatura Up: Specyfikacja wskaźnikowych struktur danych Previous: Zawartość pracy Marcin Kubica 2000-03-14