W ramach pracy opracowano i zaimplementowano algorytm rozwiązywania równań tropowych, który stał się częścią strategii dowodowej, wspomagającej automatyzację procesu dowodzenia tych obligacji (weryfikacja poprawności specyfikacji) i hipotez użytkownika (walidacja specyfikacji).
Klasyfikacja tematyczna według ACM (Association for Computer Machinery):
D.2.4 Software Engineering/(Software/Program Verification)/Formal Methods
F.3.1 Theory of Computation/Logics and Meaning of Programs/Specifying and Verifying
and Reasoning about Programs/Mechanical Verification
Słowa kluczowe: Metoda tropów (TAM), PVS, weryfikacja specyfikacji, walidacja specyfikacji.
Niniejsza praca jest poświęcona zagadnieniu weryfikacji specyfikacji systemów komputerowych zapisanych za pomocą metody tropów. Metoda tropów (ang. Trace Assertion Method) opisana w [5] jest metodą formalnej specyfikacji interfejsów moduów systemów komputerowych. Jej opis zamieszczono w rozdziale 2.
Do weryfikacji specyfikacji tropowych jest używany Prototype Verification System (PVS), w którym można dowodzić warunki gwarantujące poprawność specyfikacji. Dzięki opracowanej metodzie tłumaczenia specyfikacji tropowych do PVS, warunki poprawności są generowane przez system automatycznie. System PVS oraz sposób zanurzenia metody tropów w języku specyfikacji PVS opisano w rozdziale 3.
Najtrudniejszym zadaniem jest udowodnienie twierdzeń warunkujących poprawność specyfikacji. Nie istnieje mechanizm, który pozwalałby automatycznie dowodzić wygenerowane przez system twierdzenia, dlatego często dowodzenie jest procesem żmudnym. Możliwe jest natomiast automatyzowanie tego procesu poprzez tworzenie w PVS własnych komend (strategii dowodowych) realizujących konkretne, często złożone zadania. Tworzeniu strategii dowodowych dla metody tropów została poświęcona praca [6]. Opisano w niej strategie, które znacznie ułatwiły proces dowodzenia specyfikacji tropowych.
Praca [12] dotyczy zagadnienia walidacji specyfikacji poprzez tworzenie ich prototypów. Prototyp może posłużyć do sprawdzenia, czy semantyka specyfikacji rzeczywiście odpowiada intuicjom, które jej autor zapisał formalnie. W pracy zamieszczono opis algorytmu rozwiązywania równań tropowych. Moim zadaniem było przeniesienie tego algorytmu do systemu PVS i zastosowanie go do automatyzacji dowodzenia poprawności specyfikacji tropowych zanurzonych w PVS, w celu stworzenia narzędzia, które stanowiłoby uzupełnienie i rozszerzenie możliwości aktualnie dostępnych strategii. W rozdziale 4 opisuję zagadnienia związane z opracowaniem tego algorytmu na potrzeby PVS. Przedstawiam także sposób wykorzystania rozwiązań zastosowanych w [6].
Działanie zrealizowanego w PVS algorytmu przedstawiono w rozdziale 4 na przykładzie modułu stos (stack), bajt (byte) i ciąg bajtów (sequence). W podrozdziale 4.3 podsumowano możliwości zastosowania algorytmu rozwiązywania równań tropowych do weryfikacji poprawności specyfikacji tropowych.
Specyfikacje tropowe stosu, bajtu i ciągu bajtów zapisane w języku PVS zamieszczono w Dodatku A. Dodatek B zawiera opis parametrów powstałej strategii dowodowej oraz spis plików zawierających jej kod. Całość kodu źródłowego znajduje się na załączonej dyskietce.
Pragnę gorąco podziękować dr Janinie Mincer-Daszkiewicz za zaangażowanie i pomoc w trakcie powstawania tej pracy. Podziękowania kieruję również do mgra Marcina Engela za pomoc w rozwiązywaniu problemów związanych z systemem PVS.
Praca jest częściowo sponsorowana przez Komitet Badań Naukowych w ramach projektu badawczego nr 8 T11C 015 15.
Warunkiem koniecznym do tego, aby specyfikacja była semantycznie poprawna, jest prawidłowe użycie konstrukcji, które występują w metodzie tropów. Szczegółowe informacje zawiera raport [5]. Przedstawiamy tutaj, jako przykład, tylko niektóre warunki, które należy sprawdzić:
Najważniejszą, z naszego punktu widzenia, cechą systemu PVS jest udostępnienie użytkownikowi możliwości pisania własnych strategii dowodowych. Strategie systemowe są dosyć ogólne, często trzeba więc do konkretnych zastosowań sformułować własne. Dokumentacja systemu PVS ([11]) zawiera tylko najbardziej podstawowe informacje na temat pisania strategii dowodowych, natomiast w znikomym stopniu informuje o sposobach dostępu do formuł i wyrażeń logicznych, czy wykorzystaniu funkcji pomocniczych. Częściowo wiedzę o strukturach danych PVS i operacjach na nich można czerpać z pliku strategies.lisp, zawierającego definicje niektórych strategii. Innym sposobem jest przeglądanie z poziomu interpretera języka Common Lisp listy symboli zdefiniowanych w pakiecie PVS za pomocą poleceń apropos i describe, które pozwalają na znalezienie nazw funkcji i nazw ich argumentów, a także klas obiektów. Oczywiście w ten sposób nie można się dowiedzieć nic o semantyce znalezionych funkcji. Większość z nich ma jednak znaczące nazwy, które pozwalają na ich poprawne używanie. Cennym dokumentem na temat PVS okazała się praca A. Kreta [7], który opisał w niej dokładnie wiele struktur danych PVS i funkcji pomocniczych. Ponieważ jest to wiedza nieudokumentowana, zdobyta przez autora na podstawie jego doświadczeń z PVSem w wersji 2.1, część informacji tam zawarta jest nieaktualna z powodu zmian, które zostały wprowadzone przez autorów w kolejnych wersjach. W ostateczności można spróbować uzyskać odpowiedź na konkretne pytanie bezpośrednio od autorów systemu.
Strategie użytkownika implementujemy, tak jak większość
strategii systemowych, w języku Common Lisp Object System. Nowe strategie
definiujemy w pakiecie PVS, używając następującej składni
(aby zapoznać się z przykładami definiowania strategii można
obejrzeć plik
strategies.lisp):
(defstep nazwa-strategii
( parametry-obowiązkowe
&optional parametry-opcjonalne
&rest nazwa-parametru )
wyrażenie
dokumentacja
tekst-podczas-dowodu )
Dla parametrów opcjonalnych można podać wartość domyślną, umieszczając nazwę parametru w nawiasach razem z tą wartością, na przykład (copy t). Definicja strategii jest wyrażeniem (ang. strategy expression), które może mieć jedną z następujących postaci:
Specyfikacje zapisane w metodzie tropów tłumaczymy do języka PVS. Metoda tłumaczenia, której pełen opis znajduje się w pracy [3] (jedna z wcześniejszych prac dotyczących tej metody to [2]), została opracowana tak, aby warunki semantycznej poprawności były generowane przez PVS automatycznie jako TCCs. Każdemu modułowi o nazwie M odpowiada kilka teorii w PVS. W tym rozdziale prezentujemy więc najbardziej podstawowe informacje o tłumaczeniu, opisujemy też teorie, które powstają po przetłumaczeniu modułu do PVS. Prezentujemy także zagadnienia związane z weryfikacją poprawności i walidacją specyfikacji tropowych w PVS.
Celem tłumaczenia specyfikacji tropowych do PVS jest formalne wykazanie konkretnych właściwości specyfikacji. Po pierwsze, pokazujemy, że specyfikacja jest semantycznie poprawna (por. 2.2.2). Dla wygody będziemy używać skróconego terminu poprawność. Po drugie, sprawdzamy, czy semantyka specyfikacji jest zgodna z intuicją, czyli dokonujemy walidacji specyfikacji. Realizacja pierwszego zadania wymaga udowodnienia warunków TCC dla wszystkich teorii, tworzących specyfikację. Jeśli uda się przeprowadzić dowody wszystkich obligacji, to uznajemy że specyfikacja jest poprawna. Walidacja polega na udowodnieniu hipotez, opisujących własności specyfikowanych modułów.
Rozważmy specyfikację modułu sequence w PVS. W głównej teorii sequence_TAM, w definicji funkcji pomocniczej last_pos (znajdowanie ostatniej pozycji, na której zapisano bajt) użyto konstrukcji WHERE:
last_pos(T:ctraces):int =
COND
T = empty -> -1,
T /= empty ->
where1(lambda(T1:ctraces,p:int,b:byte_TAM.ctraces):
T = T1 o (: PUT_1(p,b) :),
lambda(T1:ctraces,p:int,b:byte_TAM.ctraces): p)
ENDCOND
Poprawne użycie tej konstrukcji wymaga, aby zawsze istniał dokładnie jeden zestaw wartości, spełniający warunek konstrukcji WHERE. System PVS generuje następującą obligację dowodową:3.3
last_pos_TCC1: OBLIGATION
FORALL (T: ctraces):
T /= empty[sequence] IMPLIES
exists1! (x: [ctraces, int, byte_TAM.ctraces]):
T = x`1 o (: PUT_1(x`2, x`3) :);
Dowód tego faktu nie jest skomplikowany, chociaż jest dość długi. Należy rozwinąć definicję where1 oraz zastosować lematy dotyczące konstrukcji iter i abstrakcyjnego typu danych sequence.
Chcemy, aby specyfikacja obiektów w module sequence była zgodna z intuicją. Na przykład, formułujemy hipotezę, że jeśli czytamy z ciągu bajtów z pozycji, na której nic nie było wcześniej zapisane, a numer tej pozycji jest mniejszy niż długość ciągu, to otrzymamy bajt zerowy:
put_get2: LEMMA
GET_ARR_1((: PUT_1(2, (: IntToByte_0(9) :)) :),1,n,byte_TAM.empty_equiv)
= 0
Mimo, że jest to fakt prosty w sformułowaniu, jego dowód jest złożony. Należy rozwinąć definicję programu dostępu GET, w której używamy m.in. konstrukcji WHERE. Wymaga to zastosowania wielu lematów. Ten i inne przykłady hipotez użytkownika omawiamy w rozdziale 4.3.
Jak już wspomnieliśmy w rozdziale 3.4.2, wykazanie odpowiednich własności specyfikacji tropowej wymaga udowodnienia wielu obligacji i hipotez. Dowodzenie jest często procesem żmudnym i długotrwałym. Wiele kroków dowodowych powtarza się. W związku z tym należy tworzyć strategie dedykowane metodzie tropów, pozwalające zredukować liczbę kroków dowodu, czyli ręcznie wpisywanych poleceń systemu dowodzącego. Kilka bardzo użytecznych strategii opisano w pracy [6]. W tym rozdziale opisujemy zagadnienia związane z projektowaniem nowej strategii dowodowej służącej do automatyzacji dowodzenia pojawiających się twierdzeń. Wybraliśmy zagadnienie rozwiązywania równań, w szczególności równań tropowych, ponieważ operator równości używany jest w specyfikacjach tropowych bardzo często. Za jego pomocą definiuje się programy dostępu, funkcję rozszerzającą, funkcję redukcji. Operator równości występuje najczęściej także przy definiowaniu predykatu kanoniczności tropu, używa się go do formułowania hipotez użytkownika. W związku z powyższym podczas dowodzenia wygenerowanych przez system warunków TCC oraz innych twierdzeń napotykamy często sekwenty zawierające formuły z równościami, kwantyfikowane egzystencjalnie. Potrzebujemy narzędzia, które będzie można wykorzystywać w takich sytuacjach. Nowa strategia będzie służyła do instancjacji (pojęcie to omawiamy w rozdz. 3.3.2) znalezionymi rozwiązaniami formuł kwantyfikowanych egzystencjalnie. W projekcie implementacji strategii wykorzystujemy algorytm zamieszczony w pracy [12], opisujemy go w podrozdziale 4.1. Przedstawiamy także strategię eq-inst?, opisaną w pracy [6]. W dalszej części rozdziału prezentujemy rozwiązanie konkretnych problemów związanych z realizacją strategii w PVS. Na końcu rozdziału przedstawiamy sposoby użycia strategii.
Nowa strategia, którą tworzymy w PVS dla specyfikacji tropowych, opiera się na opisanym w poprzednim rozdziale algorytmie rozwiązywania równań tropowych (Algorytm 1). W pierwszym punkcie przedstawimy zagadnienia, które trzeba rozważyć przed implementacją strategii i sformułujemy cele, które chcemy osiągnąć. W dalszych punktach opisujemy różne fragmenty strategii solve-equalities, przedstawiając sposoby rozwiązania problemów związanych z jej implementacją, a także znaczenie parametrów. Podane przykłady pokazują jej zastosowania. Opis wszystkich parametrów strategii znajduje się w Dodatku 7.
Chcemy, aby rozwiązywanie równań tropowych w PVS służyło do instancjacji formuł kwantyfikowanych egzystencjalnie. Do poszukiwania rozwiązań wykorzystamy Algorytm 1. Warto jednak zauważyć, że zastosowania generatora prototypów i nowej strategii są inne. Równania, które pojawiają się specyfikacjach w PVS podczas dowodu, są zwykle dość ogólne, dotyczą bowiem ogólnych własności specyfikacji. Takie równania mają często nieskończenie wiele rozwiązań, chcielibyśmy jednak móc je rozwiązywać. W odróżnieniu od generatora prototypów, nie jest więc tutaj najistotniejszą kwestią znalezienie wszystkich rozwiązań -- staramy się raczej nie ograniczać zbioru rozwiązywanych równań do zbyt wąskiej klasy, przy zachowaniu własności stopu algorytmu. Rzeczą dla nas najważniejszą jest zapewnienie, że po zastąpieniu zmiennych wartościami, pochodzącymi z przekazanych przez przez strategię rozwiązań, otrzymamy formuły, które udaje się udowodnić w PVS. Kwestią niemniej ważną jest opracowanie takiego algorytmu, który mimo wprowadzonych rozszerzeń będzie miał własność stopu. Widzimy więc, że ze względu na inne zastosowania możemy i musimy zmienić wiele elementów i założeń Algorytmu 1, a także dodać nowe, jeśli okaże się to konieczne.
Celem przeniesienia Algorytmu 1 do PVS jest projekt i implementacja odpowiedniej strategii dowodowej. Działanie strategii powinno polegać na analizie bieżącego sekwentu i utworzeniu listy kroków zawierającej polecenia instancjujące oraz wywołania strategii pomocniczych. Przed implementacją należy opracować następujące elementy, stanowiące trzon strategii:
W tym punkcie chcemy przedstawić użycie nowej strategii w różnych przypadkach. Pokażemy, że strategia jest dość ogólna, znajduje zastosowanie także przy dowodzeniu twierdzeń nie związanych z metodą tropów. Wskażemy także ograniczenia nowej strategii -- sytuacje, w których warto zastosować prostsze, wbudowane komendy, jak inst? i grind lub opisaną w pracy [6] strategię eq-inst?.
Działanie strategii solve-equalities polega na analizie nawet dość skomplikowanych wyrażeń tropowych. Dlatego też warto ją stosować, gdy formuła kwantyfikowana egzystencjalnie zawiera równanie, w którym w wyrażeniach po obu stronach występują operatory takie jak iter, o, stała empty lub konwersja typetolist. Prosta unifikacja takich wyrażeń zwykle nie powiedzie się, nie uda się też zastosowanie bardziej skomplikowanej unifikacji iteracji z listą (zaimplementowane w eq-inst?). W takiej sytuacji zwykle nie da rezultatu użycie grind lub inst?. Należy jednak pamiętać, że równości są analizowane tylko wtedy, gdy co najmniej po jednej ze stron nie występują zmienne. Gdy tak nie jest, można ręcznie dokonać instancjacji części zmiennych, a następnie ponownie użyć polecenia solve-equalities. Można także spróbować użyć strategii eq-inst?, nie nakłada ona bowiem ograniczeń na występowanie zmiennych w równościach, dlatego jest w niektórych sytuacjach skuteczniejsza od solve-equalities.
Dzięki solve-equalities dowód następującej hipotezy
(dotyczącej modułu
stack) jest krótki i nie trzeba
ręcznie instancjonować formuły podczas dowodu:
push_pop: LEMMA
exists (n,m:int, f:[int->int]):
iter[stack](1,m,lambda(i:subrange(1,m)):
if i>1 then
(: PUSH_1(f(i+1)) :)
else
(: POP_1 :)
endif) o (: PUSH_1(n+3) :)
= (: POP_1 :) o
iter[stack](1,5,lambda(i:subrange(1,5)): (: PUSH_1(i)
:))
Po zastosowaniu strategii (z domyślnymi parametrami) otrzymujemy
rozwiązanie, w którym zmiennym przyporządkowane są odpowiednio
wartości: 2, 5 oraz
LAMBDA (i: integers.int):
COND 3 = i -> 1, 4 = i -> 2, 5 = i -> 3, 6 = i -> 4, ELSE -> 4 ENDCOND
Następującego twierdzenia, bardzo prostego, nie udało się
udowodnić korzystając zarówno ze strategii grind, jak i eq-inst?.
|----
{1} EXISTS (f: [subrange(1, 1) -> int]):
empty o (: PUSH_1(f(1)) :) = (: PUSH_1(2) :)
Rule? (solve-equalities)
Solving trace equalities...,
this simplifies to:
|----
{1} empty o (: PUSH_1(COND 1 = 1 -> 2, ELSE
-> 2 ENDCOND) :) = (: PUSH_1(2) :)
Widzimy, że użycie solve-equalities pozwoliło
na instancjację formuły odpowiednim wyrażeniem.
W dowodach warunków TCC i hipotez użytkownika często występują charakterystyczne sytuacje, w których możemy wykorzystać nową strategię.
Sytuacje, gdzie można zastosować w dowodach krok solve-equalities,
to takie, gdy w twierdzeniach używana jest konstrukcja WHERE,
zdefiniowana za pomocą funkcji epsilon. Używa się wtedy
zwykle lematu epsilon_ax, co powoduje pojawienie się formuły
kwantyfikowanej egzystencjalnie w zbiorze następników sekwentu. Właśnie
taka sytuacja występuje w dowodzie hipotezy użytkownika, prezentowanej
już w p. 3.4.2.2. Pojawia się sekwent:
put_get2.1.2 :
|----
{1} EXISTS (x: [sequence_TAM.ctraces, int, byte_TAM.ctraces]):
(: PUT_1(2, (: IntToByte_0(9) :)) :) = cons(PUT_1(x`2, x`3), x`1
Rule? (solve-equalitites :copy t)
Otrzymujemy rozwiązanie, instancjacja prowadzi od razu do zakończenia
tej gałęzi dowodu4.6.
Strategia solve-equalities ma zastosowanie dla formuł bardziej złożonych, niż w poprzednim twierdzeniu (jedno równanie). Dzięki sprowadzaniu wyrażeń do postaci DNF, można dowodzić twierdzenia zawierające inne spójniki logiczne niż koniunkcja. Strategia eq-inst? nie daje takiej możliwości. Możliwość otrzymywania więcej niż jednego rozwiązania umożliwia użytkownikowi wybranie ze zbioru rozwiązań tego najwłaściwszego.
Dzięki zastosowaniu solve-equalities (z opcją :if-match
all), otrzymujemy dwa rozwiązania dla następującego twierdzenia:
a5: LEMMA
exists (t,z: traces[sequence]):
(t = empty_equiv or t o (: TRUNC_1(2) :) = z) and
z = iter[sequence](1,3,lambda(i:subrange(1,3)): (: PUT_1(i,b) :) o (: TRUNC_1(i-1) :))
Zaimplementowany algorytm rozwiązywania układów równań
pozwala na szukanie właściwej kolejności, w jakiej powinny być
rozwiązywane równania. Mamy dzięki temu swobodę w formułowaniu
definicji i twierdzeń. Zresztą trudne jest formułowanie definicji
tak, aby zawsze udawało się znaleźć podstawienie przy próbie
rozwiązywania równań po kolei.
Wprowadzenie opcji checkall pozwala na generowanie rozwiązań, dla których pewne warunki dowodzimy za pomocą innych kroków dowodowych. Takiej możliwości nie dawała strategia eq-inst?.
Dowodząc poniższe twierdzenie, używamy opcji checkall
ustawionej na wartość nil. Wynika to z obecności warunku
Canonical(x) jako jednego z członów koniunkcji. Prawdziwości
takiego wyrażenia nie jesteśmy w stanie rozstrzygnąć wewnątrz
strategii. Dlatego po znalezieniu wartości zmiennej x, spróbujemy
udowodnić ten warunek używając dodatkowych komend. Warto zauważyć,
że nie można być rozwiązywać równań po kolei --
najpierw należy rozwiązać równania drugie i trzecie, a następnie
równanie pierwsze.
stack_set :
|----
{1} EXISTS (x, y, z: traces[stack]):
x o y = z o z AND
z o (: POP_1 :) =
iter[stack](1, 1, LAMBDA (i: subrange(1, 1)): (: PUSH_1(6) :) o (: POP_1 :))
AND y = empty AND Canonical(x)
Rule? (solve-equalities :checkall nil)
Po otrzymaniu rozwiązania upraszczamy sekwent za pomocą
komendy (grind :if-match nil), w wyniku czego otrzymujemy
sekwent zawierający formułę warunkującą kanoniczność
tropu
(: PUSH_1(6), PUSH_1(6) :) (wartość
nadana zmiennej x):
|----
{1} EXISTS (n: int, f: [subrange(1, n) -> int]):
cons(stack_adt.PUSH_1(6), cons(stack_adt.PUSH_1(6), (: :))) =
iter[stack](1, n, LAMBDA (i: subrange(1, n)): (: PUSH_1(f(i)) :))
Rule?
Teraz można jeszcze raz użyć komend solve-equalities
i grind (bez dodatkowych opcji), aby doprowadzić dowód do końca.
Strategię solve-equalities można stosować do dowodzenia twierdzeń, które nie zawierają wyrażeń tropowych. Możliwość rozwiązywania układów równań, czy stosowania zmiennych złożonych powoduje, że strategia znajduje bardziej ogólne zastosowanie.
Rozpatrzmy następujący fakt:
int_lemma: LEMMA
exists (x:int, f:[int->int]):
f(2) = 10 and f(5) = 3
and 2*x + 4 = 8
and exists(y:int): y + 1 = x
Dowód przeprowadzamy, używając solve-equalities
z domyślnymi wartościami opcji. Sprawdzana jest więc prawdziwość
wszystkich członów koniunkcji. Okazuje się, że są to prawdziwe
formuły, otrzymujemy więc, w wyniku instancjacji, następujący
sekwent:
int_lemma :
|----
{1} COND 2 = 2 -> 10, 5 = 2 -> 3, ELSE -> 3 ENDCOND = 10 AND
COND 2 = 5 -> 10, 5 = 5 -> 3, ELSE -> 3 ENDCOND = 3 AND
2 * 2 + 4 = 8 AND (EXISTS (y: int): y + 1 = 2)
Rule? (grind)
Q.E.D.
Strategia solve-equalities, mimo swojej skuteczności, czasami zawodzi. Niekiedy zamiast niej można zastosować strategie systemowe (grind, inst?) lub strategię eq-inst?.
W opisywanej poniżej sytuacji nie możemy zastosować solve-equalities,
mimo iż twierdzenie wydaje się oczywiste. Wynika to z niemożności
rozwinięcia pierwszej z iteracji (dolna granica jest zmienną). Próba
unifikacji obu wyrażeń (iteracji) także się nie udaje. Okazuje
się jednak, że najlepsze w tym wypadku jest po prostu zastosowanie
strategii inst?:
test_inst :
|----
{1} EXISTS (z: int, n: int, f: [subrange(z, n) -> int]):
iter[stack](z, n, LAMBDA (i: subrange(z, n)): (: PUSH_1(f(i)) :)) =
iter[stack](1, 10, LAMBDA (i: subrange(1, 10)): (: PUSH_1(2) :))
Rule? (inst?)
Found substitution:
f: [subrange(z, n) -> int] gets LAMBDA (i: subrange(1, 10)): 2,
n: int gets 10,
z: int gets 1
Instantiating quantified variables
Znalezione podstawienie jest poprawne, wykonanie kroku grind
prowadzi do zakończenia dowodu twierdzenia.
Podsumowując, za najważniejsze cechy strategii solve-equalities, umożliwiające jej stosowanie do weryfikacji specyfikacji tropowych w PVS w wielu różnorodnych przypadkach i dające jej w wielu sytuacjach przewagę nad dotychczas istniejącymi strategiami (eq-inst? i strategie systemowe) uznajemy:
Celem pracy było zbadanie możliwości wykorzystania algorytmu rozwiązywania równań tropowych [12] do automatyzacji weryfikacji poprawności specyfikacji tropowych w PVS. Powstała strategia solve-equalities, której działanie opiera się na tym algorytmie, przeniesionym (z koniecznymi zmianami i rozszerzeniami) do systemu PVS. Wykorzystaliśmy algorytm unifikacji zaimplementowany jako część strategii eq-inst?, przedstawionej w pracy [6]. Nowa strategia okazała się dość skutecznym i elastycznym narzędziem w dowodach twierdzeń formułowanych w metodzie tropów, co pokazują zamieszczone przykłady. W większości przypadków zastępuje ona eq-inst? i umożliwia znajdowanie rozwiązań w przypadkach, gdy użycie eq-inst? nic nie wnosi. Można ją stosować także w dowodach twierdzeń nie związanych z metodą tropów, co stanowi jej istotną zaletę.
Algorytm realizowany przez nową strategię posiada ograniczenia, których usunięcie wydaje się możliwe. Ważnym zadaniem byłoby opracowanie na przykład takiej wersji, która umożliwiałaby (przy pewnych założeniach) rozwiązywanie równań tropowych w sytuacji, gdy po obu stronach równania występują zmienne. Możliwa jest także realizacja takiej wersji strategii, która operowałaby na tropach zapisanych w PVS jako skończone sekwencje (finseq), a nie listy. Z faktu, że tropy są de facto listami, korzystamy jawnie tylko w module traces. Wydaje się, że do utworzenia innej wersji strategii wystarczy tylko zamiana tego modułu.
Przydatne mogłoby się także okazać włączenie strategii solve-equalities do nowej wersji ogólnej strategii dowodowej dla metody tropów -- tam-grind [6]. Wymagałoby to dostosowania elementów tam-grind do nowej wersji systemu PVS (niestety działanie tej strategii nie jest poprawne w obecnej wersji) oraz opracowania sposobu połączenia tych elementów z nową strategią.
Podczas pracy nad dowodami niektórych faktów wykorzystywaliśmy strategie opisane w pracy [6]. Mamy nadzieję, że także strategia solve-equalities stanie się użytecznym narzędziem wspomagającym dowodzenie specyfikacji tropowych.
Poniżej prezentujemy opis wszystkich opcji strategii solve-equalities oraz fragment jej kodu umieszczony w pakiecie PVS odpowiadający za obsługę podanych parametrów. Dalej zamieszczamy spis plików zawierających kod. Na końcu prezentujemy plik pvs-strategies.
Po uruchomieniu komendy (help solve-equalities) otrzymamy następującą informację na temat strategii solve-equalities:
(SOLVE-EQUALITIES/$ &OPTIONAL (FNUM +) (CHECKALL T) (MSG T) (COPY NIL)
(IF-MATCH T) (TCC T)) :
Wszystkie parametry strategii są opcjonalne. Aby użyć strategii z wartością parametru inną niż domyślna, piszemy na przykład:
(solve-equalities :fnum 2 :tcc nil)
Znaczenie kolejnych parametrów jest następujące:
(defstep solve-equalities
(&optional
(fnum +) (checkall t) (msg t) (copy t) (if-match t) (tcc t))
(let ((fns (TAM-lib::formnums fnum))
(fns (TAM-lib::increasing-seq fns))
(steps (solve::get-step-list msg checkall fns if-match))
(tcc-step (if tcc
'(then (hide-all-but 1)
(try
(try (cond-disjoint-tcc)
(fail)
(postpone))
(skip) (postpone)))
'(postpone)))
(nums-inst (loop for s in (cdr steps)
collect
(car (cdr s)))
)
(nums-inst (remove-duplicates nums-inst))
(new-steps
(loop for s in (cdr steps)
collect
`(branch ,s
((beta)
,tcc-step ))))
(new-steps
(if copy new-steps
(cond
((null nums-inst)
new-steps) ;bez zmiany
(t
(append
new-steps
(list `(hide-exists ,nums-inst)) ))
)))
(new-steps (cons 'then new-steps))
)
new-steps
)
"Tries to instantiate given formulas.
Uses an algorithm solving TAM equalities combined with
TAM-specific version of the unification algorithm.
Analyzes a DNF form of a formula.
PARAMETERS:
Fnum: Chooses a formula to instantiate
(default is + - consequent formulas).
Checkall: if set - forces checking all formulas,
if not - only equalities are checked.
If-match: if set to t, only first solution is applied to formula,
if set to all then all found solutions are returned
(default is t).
Tcc: if set - uses cond-disjoint-tcc to prove
tccs obtained when formula is instantiated
(default t - set).
MsgOn: enables/disables messages (default is t - on).
Copy: used to retain a copy of the quantified formula
(default is nil)"
"Solving trace equalities..." )
Kod funkcji pomocniczych i strategii jest rozmieszczony w kilku plikach i pakietach:
W pliku pvs-strategies znajdują się polecenia języka Lisp, za pomocą których system PVS ładuje definicje odpowiednich strategii użytkownika. Oto jego treść:
;;;
;;; PVS-STRATEGIES - strategie uzytkownika
;;; ======================================
;;
;; zaladuj pomocnicze funkcje do ladowania bibliotek strategii
;;
(load "LOADING.lisp" :verbose nil)
;;
;; zdefiniuj zmienna *TAM-libs* i przypisz na nia liste bibliotek strategii
;;
(defvar *TAM-libs* nil)
(setq *TAM-libs* '(
"TAM-LIB.lisp"
"EQ-INST.lisp"
"GET-NEW-INST.lisp"
"INTRODUCE-LEMMA.lisp"
"EXPR.lisp"
"TRACES.lisp"
"SOLVE.lisp"
"SOLVE-EQS.lisp"
"EQ-SET.lisp"
))
;;
;; zaladuj strategie
;;
(load-TAM-libs *TAM-libs* nil)