Szukajcie a znajdziecie

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:



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:



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:



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:

• szukaj.gpr
• main.adb
• szukaj.ads
• szukaj.adb
• szukaj2.zip archiwum zawierające powyższe pliki

Tags: GNATprove