Niezawodne programowanie
Pułapki formalnej weryfikacji
22/06/13 17:50
Rozpatrzmy następującą specyfikację typów i funkcji szukaj:
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:
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:
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:
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:
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:
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:
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:
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:
- szukaj.gpr
- main.adb
- szukaj.ads
- szukaj.adb
- szukaj.zip archiwum zawierające powyższe pliki