Przykład fragmentu kodu z formalnymi komentarzami SPARK:
procedure Increment (X : in out Counter_Type); --# derives X from X; --# pre X < Counter_Type'Last; --# post X = X~ + 1;
Komentarze te precyzyjnie określają do jakich zmiennych globalnych odwołuje się dana funkcja oraz w jaki sposób wpływa ona na wartość zmiennej X (może być tylko większa o 1, nie mniejsza, ani nie równa początkowej wartości) oraz jaka musi być początkowa wartość zmiennej X (mniejsza od największej dopuszczalnej wartości Counter_Type). Deklaracje te stanowią podstawę dla formalnej weryfikacji kodu funkcji przez SPARK Examiner, który sprawdza czy wynik działania tego kodu będzie zgodny z deklaracjami formalnymi.
Zobacz też Ada (informatyka)
Linki zewnętrzne
- darmowa wersja SPARK
Kategoria:Proceduralne języki programowania