Uniwersytet Warszawski

Wydział Matematyki, Informatyki i Mechaniki

 

Strategie dowodzenia specyfikacji tropowych

 
Artur Kret
Nr albumu: 153308
Promotor: dr Janina Mincer-Daszkiewicz
 
 
Warszawa, wrzesień 1998
 
Praca magisterska napisana w Instytucie Informatyki

1. Wstęp

Przedmiotem niniejszej pracy jest zbadanie możliwości automatyzacji procesu formalnej weryfikacji poprawności specyfikacji zapisanych w metodzie tropów.

Metoda tropów [7] jest formalizmem służącym do specyfikowania interfejsów modułów systemów komputerowych. Jej opisowi poświęcono rozdział 2, w którym są także zamieszczone obligacje dowodowe warunkujące poprawność każdej specyfikacji tropowej.

Do generowania i weryfikacji obligacji będziemy wykorzystywać Prototype Verification System (w skrócie PVS [10,11,14]) przedstawiony w rozdziale 3. W tym celu zanurzymy metodę tropów w języku specyfikacji tego narzędzia (rozdział 4). Opracowana metoda [4] pozwala automatycznie generować wszystkie zidentyfikowane wcześniej warunki poprawności, dzięki czemu można sprowadzić weryfikację specyfikacji tropowych do weryfikacji ich tłumaczeń przy użyciu standardowych metod PVS. Proces ten, opisany w rozdziale 5, polega na dowodzeniu twierdzeń wygenerowanych przez system, które są odpowiednikami obligacji dowodowych.

Najtrudniejszym elementem procesu jest przeprowadzenie dowodów, co początkowo wykonywaliśmy ręcznie przy użyciu standardowych komend systemu dowodzącego PVS. Szybko odkryliśmy brak strategii systemowych, które należycie wspomagałyby dowodzenie specyfikacji tropowych. Powodowało to m.in. konieczność żmudnego, i często nudnego, powtarzania tych samych kroków dowodowych oraz owocowało dużą wrażliwością dowodów nawet na niewielkie zmiany specyfikacji.

Realizacji zadania stworzenia odpowiednich strategii dedykowanych metodzie tropów jest poświęcony rozdział 6. Analizujemy w nim fragmenty dowodów, w których dostrzec można mankamenty działania strategii systemowych oraz prezentujemy wypracowane rozwiązania umożliwiające ich uniknięcia. Cieszy fakt, że powstałe kroki dowodowe okazują się dość ogólne.

Proces przejścia ze specyfikacji tropowej do języka PVS oraz jej weryfikacja są zaprezentowane w pracy na przykładzie specyfikacji modułu stosu (oryginalna specyfikacja znajduje się w Dodatku A, natomiast jej tłumaczenie w Dodatku D). Załączniki obejmują również: bibliotekę tropową dla PVS (Dodatek C) oraz opisy wybranych strategii systemowych PVS (Dodatek B).

Część wyników pracy w postaci kodu źródłowego wybranych kroków dowodowych jest zamieszczona w Dodatku E, całość natomiast znajduje się na załączonej dyskietce.

Pragnę gorąco podziękować dr Janinie Mincer-Daszkiewicz i mgrowi Marcinowi Engelowi za inspirację tematu pracy oraz poświęcenie i nieocenioną pomoc podczas jej realizacji i redakcji.

Dziękuję również mgr Mirosławie Miłkowskiej za cenne uwagi dotyczące realizacji algorytmu unifikacji, a także mgrowi Grzegorzowi Grudzińskiemu za pomoc w zgłębianiu tajników języka Lisp.

Praca jest częściowo sponsorowana przez Komitet Badań Naukowych w ramach projektu badawczego nr 8 T11C 015 15.

Powrót do spisu treści

  
5.2 Przykład dowodzenia poprawności specyfikacji

Proces weryfikacji specyfikacji prezentujemy na przykładzie przedstawionej wcześniej specyfikacji modułu stack. Po przetłumaczeniu na język PVS otrzymujemy następujące teorie, które kolejno sprawdzamy: W dowodach stosowaliśmy głównie metodę opartą na rozwijaniu definicji, przepisywaniu termów i używaniu odpowiednich lematów wyrażających własności występujących operatorów.

Typowy dowód prezentujemy na rys. 5.1

 
  
Rysunek 5.1: Dowód hipotezy TOP(PUSH(*,1).PUSH(*,2).POP(*)) \( \searrow \protect \)=1.

\includegraphics{top_org.ps}

Analiza przeprowadzonych dowodów wykazała następujące wady ręcznego ich wykonywania przy użyciu standardowego zestawu strategii PVS: Stworzenie metod, dzięki którym system dowodzący PVS mógłby zaradzić powyższym mankamentom umożliwiłoby automatyzację procesu dowodzenia poprawności specyfikacji tropowych, co uwolniłoby użytkownika od konieczności ręcznego dowodzenia prostych twierdzeń oraz pozwoliło uzyskać większą niezależność dowodów od zmian specyfikacji.

Powrót do spisu treści

  
6.6 Ogólna strategia dowodowa dla specyfikacji tropowych - tam-grind

Mamy już do dyspozycji wszystkie elementy potrzebne do stworzenia ogólnej strategii dowodowej dla specyfikacji tropowych, którą nazwiemy tam-grind. Poniżej prezentujemy jej definicję:

  

(defstep tam-grind (&optional (lemmas "epsilon_ax") (steps nil)

                              (grind-exclude nil))

  (let( (lemmas (if (listp lemmas)

                    lemmas

                  (list lemmas)))

        (sts (cons 'then steps))

        (lms (loop for l in lemmas

                   collect

                   `(else (try (introduce-lemma ,l)

                               (else (get-new-inst? -1 :noduplicates? t

                                                    :full-inst? t)

                                     (fail))

                               (skip))

                          (skip))))

        (lms (cons 'then lms)))

    (then (prelude)

          (new-repeat*

          (then (eq-inst* :msgon t) sts lms

                (new-try (grind :if-match nil :exclude grind-exclude)

                         (skip)

                         (fail)))))))

 

Parametrami strategii są: lista nazw lematów (:lemmas) i kroków (:steps), które będą używane w trakcie dowodu oraz lista symboli, które nie będą przepisywane przez strategię grind (:grind-exclude). Na podstawie ich wartości tworzone są napisy zawierające:

Następnie są instalowane właściwe reguły przepisywania termów (prelude) i w pętli jest wykonywana instancjacja formuł równościowych (eq-inst*), podane kroki, właściwe wprowadzanie podanych lematów oraz przepisywanie termów odpowiednio dostosowane do naszych potrzeb: bez zgadywania instancjacji (źle działało dla formuł, które obecnie poprawnie obsługuje eq-inst?) i z wyłączeniem przepisywania podanych symboli. Kroki wykonywane w pętli zostały tak zapisane, aby, zgodnie z uwagą z poprzedniej sekcji, ich wykonanie kończyło się wprowadzeniem nowych formuł lub było równoważne krokowi pustemu. Użytkownik powinien zadbać, aby wymagania te spełniały także kroki podane przez niego w opcji :steps.

O skuteczności tam-grind decyduje właściwa parametryzacja twierdzeniami oraz dedykowanymi krokami dowodowymi. Ich odpowiedni dobór pozwala automatyzować dowody prostych twierdzeń.

Na rys. 5.1 przestawiliśmy dowód faktu TOP(PUSH(*,1).PUSH(*,2).POP(*))\( \searrow \)=1 wykonany za pomocą standardowych strategii PVS. Dowód był dość długi, powtarzały się podobne kroki dowodowe, użyto kilku twierdzeń pomocniczych, których instancjacje wykonał system przy niewielkiej ingerencji użytkownika, natomiast instancjacje warunków TCC wygenerowanych w ich wyniku wykonano całkowicie ręcznie. Zastosowanie nowych strategii opisywanych w poprzednich sekcjach daje znaczne jego uproszczenie (rys. 6.1): dowód sprowadza się do rozwijania definicji, przepisywania termów i wprowadzania właściwych instancji lematu epsilon_ax. Stąd już tylko krok dzieli nas od pełnej automatyzacji osiągniętej przez zastosowanie tam-grind z opcją :lemmas "epsilon_ax" (rys. 6.2).

  
Rysunek 6.1: Dowód TOP(PUSH(*,1).PUSH(*,2).POP(*)) \( \searrow \protect \)=1 przeprowadzony z użyciem nowych strategii.

\resizebox*{0.6\textwidth}{0.75\textheight}{\includegraphics{top_nowe.ps}}



  
Rysunek 6.2: Dowód TOP(PUSH(*,1).PUSH(*,2).POP(*)) \( \searrow \protect \)=1 przeprowadzony z użyciem tam-grind.

\resizebox*{0.25\textwidth}{0.07\textheight}{\includegraphics{top_tam-grind.ps}}


Lemat epsilon_ax jest na tyle często stosowany (każda definicja zawierająca konstrukcję WHERE wymaga jego użycia podczas dowodu), że wpisaliśmy go w definicji strategii jako wartość domyślną (ustawienie to można zmienić podając jako wartość :lemmas nil lub listę nazw lematów nie zawierających "epsilon_ax").

Strategię można też parametryzować krokami dowodowymi. Poniżej prezentujemy dwa przykłady takich kroków:

Oba kroki powstały w celu automatyzacji fragmentów dowodów i mogą być używane zarówno podczas ręcznego dowodzenia, jak również do sparametryzowania strategii ogólnej. Poniżej prezentujemy dwa twierdzenia, których dowody przeprowadziliśmy z jej użyciem:


  
Rysunek 6.3: Oryginalny dowód POP_ARR_1_TCC1.

\includegraphics{pop-tcc-org.ps}



  
Rysunek 6.4: Dowód POP_ARR_1_TCC1 z wykorzystaniem tam-grind.

\resizebox*{0.9\textwidth}{0.22\textheight}{\includegraphics{pop-tcc-auto.ps}}


Powrót do spisu treści

 

6.8 Przykład automatyzacji dowodzenia poprawności specyfikacji

Po zainstalowaniu nowych strategii w systemie, zostały one wykorzystane do automatyzacji procesu dowodzenia poprawności specyfikacji modułu stack, który poprzednio przeprowadziliśmy w większości ręcznie, wykorzystując standardowe strategie PVS (por. pkt. 5.2).

W poszukiwaniu właściwych parametrów strategii ogólnej przeanalizowaliśmy wykonane wcześniej dowody pod kątem używanych lematów i kroków dowodowych dedykowanych do wykonywania pewnych małych fragmentów dowodów. Następnie z otrzymanej listy twierdzeń usunęliśmy lematy, które będą zainstalowane jako reguły systemu przepisywania termów przez strategię prelude. Ostatnią fazą było testowanie.

Przeprowadzone testy doprowadziły do ustalenia właściwych parametrów strategii ogólnej:

(tam-grind :lemmas ("epsilon_ax" "SUBTYPE_TCC1") :steps ((unique)) :grind-exclude "unique?"),

gdzie SUBTYPE_TCC1 jest nazwą warunku TCC powstającego podczas weryfikacji teorii stack_TAM, który wyraża sensowność i redukowalność do siebie samego każdego tropu kanonicznego:

SUBTYPE_TCC1: OBLIGATION (FORALL (x: ctraces): Feasible(x) AND Reduce(x) = x).

Ten wariant strategii najlepiej wspomagał automatyczne dowodzenie twierdzeń. Zastosowanie go do specyfikacji stosu zaowocowało w poszczególnych teoriach uproszczeniem wielu dowodów:

Należy zwrócić uwagę, że dowody, których długość skróciła się do kilku kroków (1-3) są dość różnorodne: od prostych twierdzeń o różnowartościowości konstruktorów abstrakcyjnego typu danych (teoria stack_adt_aux) do bardziej skomplikowanych z zakresu walidacji specyfikacji (hipotezy hyp1-hyp7 z teorii stack_hyp).

Ważne jest także spostrzeżenie, że użycie strategii w dowodach, w których nie przynosiło uproszczeń, na ogół nie powodowało również ich komplikacji.

Powrót do spisu treści

 

  
7. Podsumowanie

Celem niniejszej pracy było zbadanie możliwości automatyzacji procesu formalnej weryfikacji poprawności specyfikacji tropowych w systemie PVS. Wynikiem są opracowane strategie, za pomocą których pomyślnie zautomatyzowano część dowodów twierdzeń powstających podczas sprawdzania poprawności specyfikacji stosu. Napisanie tych kroków dowodowych wymagało znajomości języka Common Lisp i dogłębnego poznania kodu źródłowego standardowych reguł systemu. Pozytywne zakończenie prac daje nadzieję na dalszą automatyzację procesu dowodzenia poprawności oraz potwierdza słuszność wyboru PVS jako narzędzia weryfikującego, którego użycie pozwala również wykryć szereg błędów koncepcyjnych specyfikacji (np. błędna postać tropu kanonicznego, błędne definicje programów dostępu, niespójność, zła modularyzacja).

Powstały zestaw dedykowanych dla TAM kroków dowodowych i twierdzeń zachęca do zrealizowania postulowanego od dawna połączenia edytora specyfikacji z wybranym systemem dowodzenia twierdzeń.

Zdajemy sobie sprawę, że biblioteka narzędzi tropowych dla PVS nie jest jeszcze kompletna i będzie wymagała rozszerzenia. Potwierdzają to rozpoczęte badania nad automatyzacją weryfikacji fragmentów specyfikacji unixowego systemu plików [8], których dokończenie pozostawiamy kontynuatorom tej pracy.

Opracowane na potrzeby specyfikacji tropowych strategie okazały się dość ogólne i przyczyniają się one do zwiększenia możliwości automatyzacji dowodów przez PVS. Być może ich realizacja, ze względu na brak dokumentacji, nie jest najlepsza, natomiast idee wydają się celne i nowatorskie, dlatego zamierzamy poddać je dyskusji na szerszym forum użytkowników tego systemu [5].

Podczas pracy zauważyliśmy kilka poważniejszych błędów PVS, których część została już zgłoszona, natomiast resztę wraz z postulatami dotyczącymi np. użyteczniejszej postaci twierdzeń o różnowartościowości konstruktorów ADT czy specjalnego traktowania standardowych podtypów (np. subrange), zamierzamy przesłać autorom po zakończeniu prac.

Powrót do spisu treści

Literatura

[1] M. Archer, C. Heitmeyer. Human-style theorem proving using PVS, E. Gunter, A. Felty (ed.), Theorem Proving in Higher Order Logics (TPHOLs'97), volume 1275 of Lecture Notes in Computer Science, pages 33-48. Springer-Verlag, 1997.

[2] M. Archer, C. Heitmeyer, S. Sims. TAME: A PVS Interface to Simplify Proofs for Automata Models. Praca zaprezentowana na User Interfaces for Theorem Provers (UITP'98), Eindhoven University of Technology, 13-15 czerwca 1998.

[3] W. Bartussek, D.L. Parnas.  Using Traces to Write Abstract Specifications for Software Modules,  Proc. 2nd Conference of European Cooperation in Informatics, volume 65 of Lecture Notes in Computer Science, pages 211-236. Springer-Verlag, 1978.

[4] M. Engel, M. Iglewski, J. Mincer-Daszkiewicz. Generating PVS Proof Obligations for TAM Specifications, Proceedings of the CS&P'97 Workshop, pages 55-66. Warsaw University, 6-7 October 1997.

[5] M. Engel, A. Kret, J. Mincer-Daszkiewicz. Increasing Automation Capabilities of the PVS Theorem Prover, Proceedings of the CS&P'98 Workshop, pages 64-75. Humboldt-Universitat zu Berlin, 28-30 September 1998.

[6] M. Iglewski, M. Kubica, J. Madey. An Editor for the Trace Assertion Method, M. Zaremba (ed.), Proceedings of the 10th International Conference of CAD/CAM, Robotics and Factories of the Future: CARs&FOF'94, pages 876-881. OCRI, Ottawa, Ontario, Canada, 1994.

[7] M. Iglewski, M. Kubica, J. Madey, J. Mincer-Daszkiewicz, K. Stencel. TAM'97: the Trace Assertion Method of Module Interface Specification. Reference Manual. Technical Report TR 97-01 (238), Institute of Informatics, Warsaw University, January 1997.

[8] P. Kołodziejski, M. Majewska. Specyfikacja unixowego systemu plików w metodzie tropów. Praca magisterska, Instytut Informatyki, Uniwersytet Warszawski, 1996.

[9] S. Owre, J. Rushby, N. Shankar. PVS: A Prototype Verification System, Deepak Kapur (ed.), 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748-752. Springer-Verlag, June 1992.

[10] S. Owre, N. Shankar, J. Rushby. The PVS Specification Language (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, April 1993.

[11] S. Owre, N. Shankar, J. Rushby. User Guide for the PVS Specification and Verification System (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, March 1993.

[12] T. Reps, T. Teitelbaum. The Synthesizer Generator. A System for Constructing Language-based Editors, D. Gries (ed.), Text and Monographs in Computer Science. Springer-Verlag, Berlin, 1989.

[13] Selecting Sequent Formulas in PVS Proof Strategies. Dokument jest dostępny w formacie HTML pod adresem http://www.csl.sri.com/pvs.html, 1998.

[14] N. Shankar, S. Owre, J. Rushby. The PVS Proof Checker: A Reference Manual (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.

[15] G.L. Steele Jr. Common Lisp the Language. Digital Press, wydanie drugie, 1990. Książka jest dostępna w formacie HTML pod adresem AI.Repository@cs.cmu.edu.

[16] R. Wilensky. Common LISPcraft. W. W. Norton & Company, New York, London, 1986.

Powrót do spisu treści

Artur Kret

1998-10-12