Next: Zawartość pracy Up: Wstęp Previous: Wstęp
Teza pracy
Celem niniejszej pracy jest wypełnienie wspomnianej luki między metodami formalnych specyfikacji, a dość powszechnie stosowanymi wskaźnikowymi strukturami danych. Chcemy zaproponować metodę specyfikacji wskaźnikowych struktur danych oraz metodę weryfikacji programów względem takich specyfikacji.Badamy przydatność kilku formalizmów do specyfikowania zarówno wskaźnikowych struktur danych, jak i operacji modyfikujących te struktury. Przedstawiamy też własną propozycję formalizmu służącego do takich celów. Dokonujemy ich porównania na podstawie siły wyrazu oraz zwięzłości i czytelności specyfikacji przykładowych struktur danych.
Przedstawiamy też wariant logiki Hoare'a [Apt81], służącej do weryfikacji tzw. while-programów względem specyfikacji wyrażonych w wybranym przez nas formalizmie. Dowodzimy, że przedstawiony system wnioskowania jest poprawny i zupełny w sensie Cook'a [Coo78].
Tezą tej pracy jest więc stwierdzenie, że istnieje formalizm pozwalający na względnie zwięzłe specyfikowanie wskaźnikowych struktur danych i weryfikowanie programów względem specyfikacji zapisanych w tym formalizmie.
Marcin Kubica 2000-03-14