Niezawodne programowanie

GNATprove
Niezawodne programowanie::SPARK

Ciąg Fibonacciego

15/12/15 19:18
referral_campaign_blog

fibonacci.ads



pragma SPARK_Mode(on);

function Fibonacci (N : Natural) return Natural
  with
    Pre => N <= 46,
    Contract_Cases =>
      (N = 0  => Fibonacci'Result = 0,
       N = 1  => Fibonacci'Result = 1,
       others => Fibonacci'Result = Fibonacci(N - 1) + Fibonacci(N - 2));



fibonacci.adb



 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
pragma SPARK_Mode(on);

function Fibonacci (N: Natural) return Natural
is
   X : Natural := 0;
   Y : Natural := 1;
   Z : Natural := 1;
begin
   case N is
      when 0 =>
         return 0;
      when 1 =>
         return 1;
      when others =>
         for I in 2 .. N loop
            Z := X + Y;
            pragma Loop_Invariant (X = Fibonacci(I-2)
                                   and Y = Fibonacci(I-1)
                                   and Z = Fibonacci(I));
            X := Y;
            Y := Z;
         end loop;
         return Z;
   end case;
end Fibonacci;



github repozytorium

Tags:

Dowodzenie twierdzeń

26/06/13 17:58
GNATprove używa domyślnie programu alt-ergo do dowodzenia poprawności programu.

Pliki z twierdzeniami do udowodnienia mają prostą składnię.

Przykład 1

W pliku test1.why wpisano:

logic p, q: prop

axiom a1: p and q

goal g: p

Zdefiniowano w nim dwie zmienne zdaniowe p i q oraz aksjomat p and q.

Zadano również cel do udowodnienia w postaci formuły p.

Poniżej pokazano sposób uruchomienia programu alt-ergo dla pliku test1.why:

$ alt-ergo test1.why
File "test1.why", line 5, characters 1-10:Valid (0.0132) (0)

Jak widać została wykazana prawdziwość celu (wykazano wynikanie celu g z aksjomatu a1).

Przykład 2

W pliku test2.why wpisano:

logic p, q: prop

axiom a2: p or q

goal g: p

Tym razem aksjomat ma postać p or q.

Po uruchomieniu programu alt-ergo:

$ alt-ergo test2.why
File "test2.why", line 5, characters 1-10:I don't know

przekonamy się, że nie był on w stanie wyprowadzić celu g z aksjomatu a2.

Przykład 3

Ciekawą własnością programu alt-ergo jest ta, że gdy uda mu się udowodnić cel, to powiada Valid a w każdym innym przypadku, odpowiada I don’t know (nawet wtedy gdy cel w oczywisty sposób nie wynika z aksjomatów).

W pliku test3.why wpisano:

goal g: false

Oczywiście, fałszywy cel nie jest możliwy do udowodnienia, jednak program alt-ergo odpowiada z rozbrajającą szczerością:

$ alt-ergo test3.why
File "test3.why", line 1, characters 1-14:I don't know

Przykład 4

Rozpatrzmy klasyczny przykład z logiki pierwszego rzędu. Zdefiniujemy dziedzinę domain, dwa predykaty man i mortal oraz dwie stałe w dziedzinie socrates i zeus:

type domain

logic man : domain -> prop

logic mortal : domain -> prop

logic socrates : domain

logic zeus : domain

Przyjmiemy dwa aksjomaty:
  • A1: Socrates jest człowiekiem.
  • A2: Każdy człowiek jest śmiertelny.

Zapiszemy je następująco:

axiom A1: man(socrates)

axiom A2: forall x : domain. man(x) -> mortal(x)

Na koniec zadamy dwa cele do udowodnienia:
  • G1: Sokrates jest śmiertelny.
  • G2: Zeus jest śmiertelny.

Co zapisujemy następująco:

goal G1: mortal(socrates)

goal G2: mortal(zeus)

Wszystko umieścimy w pliku test4.why.

Kiedy uruchomimy program alt-ergo otrzymamy następujące odpowiedzi:

$ alt-ergo test4.why
File "test4.why", line 15, characters 1-26:Valid (0.0117) (0)
File "test4.why", line 17, characters 1-22:I don't know

Jak widać pierwszy cel mortal(socrates) został udowodniony, natomiast program alt-ergo nie był w stanie udowodnić drugi cel mortal(zeus).

Udostępnione pliki:

Więcej przykładów na stronie programu alt-ergo:

Tags: ,

Dzielenie całkowite

25/06/13 17:57
Rozpatrzmy następującą specyfikację pakietu Divide:

Zrzut ekranu 2013-06-25 o 21.38.40

Znajduje się w nim specyfikacja procedury Div o dwóch parametrach wejściowych M i N, oraz dwóch parametrach wyjściowych Q i R.

Warunek końcowy (M = Q * N + R) and (R < N) and (R >= 0) wyraża, że Q jest ilorazem całkowitym M przez N, a R jest resztą z dzielenia M przez N.

W definicji procedury Div należy podać niezmiennik pętli, bez którego program GNATprove nie byłby w stanie dowieść poprawności programu:

Zrzut ekranu 2013-06-25 o 21.39.46

O poprawności niezmiennika można przekonać się przyjmując następujące oznaczenia:
  • Q, R stare wartości zmiennych z poprzedniej iteracji (lub zainicjowane przed pętlą),
  • Q’, R’ nowe wartości zmiennych wyznaczone w danej iteracji.

Przy pierwszym przebiegu pętli niezmiennik jest oczywiście spełniony ponieważ:
  • M = Q * N + R = 0 * N + M = M
  • R = M >= 0

Między wartościami Q i R a Q’ i R’ zachodzą następujące zależności:
  • Q’ = Q + 1
  • R’ = R - N

Przy każdym kolejnym przebiegu pętli:
  • M = Q * N + R = (Q’ - 1) * N + (R’ + N) = Q’ * N - N + R’ + N = Q’ * N + R’
  • R’ = R - N >= 0, bo gdyby R < N, to nastąpiłoby wcześniej wyjście z pętli instrukcją exit

O poprawności programu można przekonać się wybierając w środowisku GPS z menu Prove opcję Prove All.

Poniżej przedstawiono fragment wyników z programu GNATprove:

divide.adb:9:10: info: loop invariant initialization proved [loop_invariant_initialization]
divide.adb:9:10: info: loop invariant preservation proved [loop_invariant_preservation]
divide.adb:9:39: info: overflow check proved [overflow_check]
divide.adb:9:43: info: overflow check proved [overflow_check]
divide.adb:11:17: info: overflow check proved [overflow_check]
divide.adb:12:17: info: overflow check proved [overflow_check]
divide.ads:6:14: info: postcondition proved [postcondition]
divide.ads:6:21: info: overflow check proved [overflow_check]
divide.ads:6:25: info: overflow check proved [overflow_check]

Udostępnione pliki:

Tags:

GNATprove w akcji

23/06/13 17:53


Warto obejrzeć powyższy film w trybie HD na pełnym ekranie.

Udostępnione pliki:

Tags:

Szukajcie a znajdziecie

22/06/13 19:52
Powróćmy do przykładu z funkcją poszukującą zadanej wartości w tablicy.

Aby udowodnić poprawność funkcji szukaj dodamy w jej specyfikacji warunek wstępny:

Zrzut ekranu 2013-06-22 o 21.19.47

Kontrakt Pre => (for some i in Indeks => tablica(i) = wartosc) wyraża warunek, że w chwili wywołania funkcji szukaj co najmniej jeden element tablicy ma zadaną wartość.

Program GNATprove, mimo dopisania warunku wstępnego, nie jest w stanie udowodnić  warunku końcowego przy następującej implementacji:

Zrzut ekranu 2013-06-22 o 13.08.01

Poniżej zamieszczono informacje z programu GNATprove:

szukaj.adb:17:17: info: range check proved [range_check]
szukaj.ads:11:14: postcondition not proved, requires tablica(szukaj'Result) = wartosc [postcondition]

Aby program GNATprove był w stanie udowodnić wynikanie warunku końcowego z warunku początkowego trzeba mu pomóc dopisując w kodzie niezmiennik pętli:

Zrzut ekranu 2013-06-22 o 21.34.52

Warunek i = Indeks'First or else (for all j in Indeks'First..i-1 => tablica(j) /= wartosc) zachodzi za każdym przebiegiem pętli. Wyraża on, że albo i jest pierwszą pozycją w tablicy albo na wszystkich wcześniejszych pozycjach nie występuje szukana wartość.

Po dopisaniu niezmiennika pętli, program GNATprove automatycznie dowodzi poprawność wszystkich zakresów, niezmiennika pętli i warunku końcowego:

szukaj.adb:11:10: info: loop invariant initialization proved [loop_invariant_initialization]
szukaj.adb:11:10: info: loop invariant preservation proved [loop_invariant_preservation]
szukaj.adb:15:40: info: index check proved [index_check]
szukaj.adb:16:17: info: range check proved [range_check]
szukaj.ads:11:14: info: postcondition proved [postcondition]

Warunek końcowy jest udowodniony nawet w przypadku niemożliwości udowodnienia warunku wstępnego.

Udostępnione pliki:

Tags:

Pułapki formalnej weryfikacji

22/06/13 17:50
Rozpatrzmy następującą specyfikację typów i funkcji szukaj:

Zrzut ekranu 2013-06-22 o 12.36.03

Kontrakt Post => tablica(szukaj'Result) = wartosc gwarantuje, że po zakończeniu działania funkcji, zwracana jest pozycja w tablicy, gdzie występuje zadana wartość.

Rozpocznijmy od następującej implementacji funkcji szukaj:

Zrzut ekranu 2013-06-22 o 12.55.12

Program GNATprove udowodnił warunek końcowy (postcondition) ale jednocześnie stwierdził, że podczas zwiększania wartości zmiennej może nastąpić przekroczenie zakresu (range_check):

szukaj.adb:11:16: range check not proved [range_check]
szukaj.ads:10:14: info: postcondition proved [postcondition]

Spełnienie warunku końcowego wynika, z tego, że po wyjściu z pętli while, jeśli tylko ono nastąpi, zachodzić będzie warunek tablica(i) = wartosc.

Druga implementacja funkcji szukaj stara się zabezpieczyć przed przekroczeniem zakresu:

Zrzut ekranu 2013-06-22 o 13.08.01

Tym razem program GNATprove potwierdził poprawność zakresów ale stwierdził, że może nie zostać spełniony warunek końcowy:

szukaj.adb:11:16: info: range check proved [range_check]
szukaj.ads:10:14: postcondition not proved, requires tablica(szukaj'Result) = wartosc [postcondition]

Oczywiście miał on rację, gdyż w przypadku kiedy żaden z elementów tablicy nie ma poszukiwanej wartości, zostanie zwrócona niepoprawna pozycja Indeks’Last.

Aby temu zaradzić sformułujmy trzecią implementację funkcji szukaj:

Zrzut ekranu 2013-06-22 o 13.16.15

Tym razem przed zwróceniem pozycji sprawdzane jest czy znajduje się na niej zadana wartość, natomiast jeśli zadana wartość nie występuje w tablicy, to zgłaszany jest wyjątek Constraint_Error.

Jednak w ostatniej implementacji funkcja zgłasza wyjątek i nie może być formalnie zweryfikowana przez program GNATprove (funkcje zgłaszające wyjątki nie należą do tzw. zbioru Alfa).

Do głowy przychodzi jeszcze drugi pomysł na obsłużenie sytuacji gdy zadana wartość nie występuje w tablicy. Otóż funkcja szukaj mogłaby zwracać logiczną stałą True gdy znaleziono pozycję (False w przeciwnym przypadku), a dodatkowo, trzecim parametrem w trybie out, oddawać znalezioną pozycję.

Jednak funkcja z parametrem out nie jest czystą funkcją (impure function). Ona również nie może być formalnie zweryfikowana programem GNATprove (nieczyste funkcje nie należą do zbioru Alfa).

Dopisane: jest jeszcze trzecia możliwość. Funkcja szukaj może zwracać rekord złożony z dwóch pól: informacji czy znaleziono wartość i pozycji. Ten przypadek opisano w SPARK 2014 Users Guide.

Udostępniane pliki:

Tags: