Niezawodne programowanie
Dzielenie całkowite
25/06/13 17:57
Rozpatrzmy następującą specyfikację pakietu Divide:
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:
O poprawności niezmiennika można przekonać się przyjmując następujące oznaczenia:
Przy pierwszym przebiegu pętli niezmiennik jest oczywiście spełniony ponieważ:
Między wartościami Q i R a Q’ i R’ zachodzą następujące zależności:
Przy każdym kolejnym przebiegu pętli:
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:
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:
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:
- divide.gpr
- divide.ads
- divide.adb
- divide.zip archiwum zawierające powyższe pliki