Niezawodne programowanie
Tak proste, że aż niepoprawne
03/07/13 17:59
Przyjrzyjmy się następującej funkcji w języku C, którą zaczerpnęliśmy ze standardowej biblioteki glibc:
Przy braku jakiejkolwiek formalnej specyfikacji możemy domyślać się, że powyższa funkcja oblicza wartość bezwzględną (inaczej moduł) liczby całkowitej i.
Z kursów matematyki wiemy, że wartość bezwzględna jest nieujemna. Możemy to wyspecyfikować w języka Ada 2012 następująco (nazwa abs jest w języka Ada zarezerwowanym słowem kluczowym):
Zaimplementujemy funkcję av podobnie do funkcji abs z biblioteki glibc:
Po uruchomieniu programu GNATprove otrzymujemy następujące komunikaty:
analyzing absolute.av, 2 checks
absolute.adb:6:29: overflow check not proved [overflow_check]
absolute.ads:4:14: postcondition not proved, requires av'Result >= 0 [postcondition]
Jak widać nie udało się dowieść poprawności programu w następujących miejscach:
Po chwili zastanowienia dociera do nas, że typ Integer ma wartości z zakresu Integer’First .. Integer’Last, który jest niesymetrycznie rozmieszczony względem 0.
Wartość -Integer’First jest o jeden większa od wartości Integer’Last i jako taka nie może być poprawnie wyrażona w typie Integer. Z arytmetyki w kodzie uzupełnieniowym do dwóch wynika, że -Integer’First jest równe Integer’First, a zatem wartość przeciwna do liczby ujemnej może być liczbą ujemną!
Aby funkcja obliczająca wartość bezwzględną z liczby całkowitej spełniła formalną specyfikację, należy zdefiniować podtyp Calkowite typu Integer:
Musimy również poprawić jej implementację:
Tym razem program GNATprove nie zgłasza żadnych zastrzeżeń.
Na zakończenie sprawdźmy jak zachowuje się operacja abs. W tym celu zamieśćmy w pliku main.adb następujący kod:
Podczas kompilacji otrzymujemy następujące ostrzeżenia o tym, że wartość przeciwna do najmniejszej całkowitej nie mieści się w zakresie:
main.adb:5:08: warning: value not in range of type "Ada.Text_Io.Integer_Io.Num" from instance at a-inteio.ads:18
main.adb:5:08: warning: "Constraint_Error" will be raised at run time
Faktycznie, po uruchomieniu programu zostaje w wierszu 5 zgłoszony wyjątek CONSTRAINT_ERROR:
raised CONSTRAINT_ERROR : main.adb:5 range check failed
A co z funkcją abs w języku C?
Cóż, przy braku typów okrojonych i braku kontroli zakresów wartości w C, programiści skazani są na korzystania z niepoprawnej funkcji bibliotecznej…
Udostępnione pliki:
Przy braku jakiejkolwiek formalnej specyfikacji możemy domyślać się, że powyższa funkcja oblicza wartość bezwzględną (inaczej moduł) liczby całkowitej i.
Z kursów matematyki wiemy, że wartość bezwzględna jest nieujemna. Możemy to wyspecyfikować w języka Ada 2012 następująco (nazwa abs jest w języka Ada zarezerwowanym słowem kluczowym):
Zaimplementujemy funkcję av podobnie do funkcji abs z biblioteki glibc:
Po uruchomieniu programu GNATprove otrzymujemy następujące komunikaty:
analyzing absolute.av, 2 checks
absolute.adb:6:29: overflow check not proved [overflow_check]
absolute.ads:4:14: postcondition not proved, requires av'Result >= 0 [postcondition]
Jak widać nie udało się dowieść poprawności programu w następujących miejscach:
- możliwe jest przekroczenie zakresu typu Integer przy wyliczaniu wartości -x;
- możliwe jest naruszenie kontraktu av’Result >= 0.
Po chwili zastanowienia dociera do nas, że typ Integer ma wartości z zakresu Integer’First .. Integer’Last, który jest niesymetrycznie rozmieszczony względem 0.
Wartość -Integer’First jest o jeden większa od wartości Integer’Last i jako taka nie może być poprawnie wyrażona w typie Integer. Z arytmetyki w kodzie uzupełnieniowym do dwóch wynika, że -Integer’First jest równe Integer’First, a zatem wartość przeciwna do liczby ujemnej może być liczbą ujemną!
Aby funkcja obliczająca wartość bezwzględną z liczby całkowitej spełniła formalną specyfikację, należy zdefiniować podtyp Calkowite typu Integer:
Musimy również poprawić jej implementację:
Tym razem program GNATprove nie zgłasza żadnych zastrzeżeń.
Na zakończenie sprawdźmy jak zachowuje się operacja abs. W tym celu zamieśćmy w pliku main.adb następujący kod:
Podczas kompilacji otrzymujemy następujące ostrzeżenia o tym, że wartość przeciwna do najmniejszej całkowitej nie mieści się w zakresie:
main.adb:5:08: warning: value not in range of type "Ada.Text_Io.Integer_Io.Num" from instance at a-inteio.ads:18
main.adb:5:08: warning: "Constraint_Error" will be raised at run time
Faktycznie, po uruchomieniu programu zostaje w wierszu 5 zgłoszony wyjątek CONSTRAINT_ERROR:
raised CONSTRAINT_ERROR : main.adb:5 range check failed
A co z funkcją abs w języku C?
Cóż, przy braku typów okrojonych i braku kontroli zakresów wartości w C, programiści skazani są na korzystania z niepoprawnej funkcji bibliotecznej…
Udostępnione pliki:
- absolute.gpr
- absolute.ads
- absolute.adb
- main.adb
- absolute.zip archiwum zawierające powyższe pliki