Niezawodne programowanie
Kontrakty
22/06/13 15:04
Jedną z najważniejszych nowości w języku Ada 2012 są kontrakty umożliwiające formułowanie warunków wstępnych i końcowych dla procedur i funkcji.
Przy specyfikacji podprogramu (procedury lub funkcji) można we frazie rozpoczynającej się słowem kluczowym with podać warunek wstępny (Pre) jaki powinny spełniać parametry podprogramu w chwili wywołania podprogramu oraz końcowy (Post) jaki powinny spełniać parametry i wyliczony wynik w chwili zakończenia działania podprogramu.
Przykład specyfikacji warunków wstępnych i końcowych:
W powyższym przykładzie użyto funkcji Is_Empty i Is_Full, które dla danego stosu S sprawdzają czy jest on, odpowiednio, pusty (nie można pobrać z niego elementu) lub pełny (nie można na niego włożyć więcej elementów).
Wśród narzędzi dostępnych na stronach firmy AdaCore znajduje się między innymi program GNATprove, który służy do formalnej weryfikacji czy program spełnia wszystkie podane w specyfikacji warunki (zakresy indeksów, zakresy wartości typów, kontrakty, niezmienniki pętli i asercje).
Umożliwia to statyczną analizę kodu, tzn. sprawdzanie jego poprawności bez potrzeby kompilowania i uruchamiania.
Należy pamiętać o tym, że testowanie programu jedynie sprawdza czy jest błąd w programie, natomiast nie potrafi wykazać, że błędu nie ma.
Analiza statyczna potrafi formalnie dowieść, że w programie nie ma błędu.
Przy specyfikacji podprogramu (procedury lub funkcji) można we frazie rozpoczynającej się słowem kluczowym with podać warunek wstępny (Pre) jaki powinny spełniać parametry podprogramu w chwili wywołania podprogramu oraz końcowy (Post) jaki powinny spełniać parametry i wyliczony wynik w chwili zakończenia działania podprogramu.
Przykład specyfikacji warunków wstępnych i końcowych:
W powyższym przykładzie użyto funkcji Is_Empty i Is_Full, które dla danego stosu S sprawdzają czy jest on, odpowiednio, pusty (nie można pobrać z niego elementu) lub pełny (nie można na niego włożyć więcej elementów).
Wśród narzędzi dostępnych na stronach firmy AdaCore znajduje się między innymi program GNATprove, który służy do formalnej weryfikacji czy program spełnia wszystkie podane w specyfikacji warunki (zakresy indeksów, zakresy wartości typów, kontrakty, niezmienniki pętli i asercje).
Umożliwia to statyczną analizę kodu, tzn. sprawdzanie jego poprawności bez potrzeby kompilowania i uruchamiania.
Należy pamiętać o tym, że testowanie programu jedynie sprawdza czy jest błąd w programie, natomiast nie potrafi wykazać, że błędu nie ma.
Analiza statyczna potrafi formalnie dowieść, że w programie nie ma błędu.