Do pre and post conditions take the place of in function validation?

user_7061612 0
Viewed 287

I have been trying to learn the basics of using SPARK and I have got my head round using the pre and post conditions, but I am unsure whether they take the place of validation? for example a function for a plane that will not switch into takeoff mode unless all doors are closed and locked. Would I need to add code to the procedure body to stop this behaviour or are the pre and post conditions enough? It's unclear to me because none of my course tutorials actually do so, but when I test the procedures, I am not restricted from violating the conditions.

spark-formal-verification spark-ada formal-methods ada formal-verification
3 Answers

The first: if you use GNAT compiler, you have to add flag -gnata to compiler flags or use configuration file for GNAT with pragma Assertion_Policy(Check); to enable check for Pre- and Post-conditions. Without one of these options, all checks are ignored. This is why you are allowed to violate them.

Preconditions take place right before the selected subprogram is executed. For example, the function declared as:

function Add(A, B: Positive) return Positive is (A + B) with
   Pre => A < 10;

This precondition will be checked before the function will be executed. For example:

I := Add(2, 2);
Put_Line(Positive'Image(I)); -- prints 4 as expected
begin
   I := Add(10, 2); -- Crash, exception on violation of precondition
exception
   when ASSERT_FAILURE =>
      Put_Line(Positive'Image(I)); -- prints 4
end;

Postconditions are checked on subprograms after their execution. Another example:

procedure Increment(A: in out Positive) with
   Post => A < 20 is
begin
   A := A + 1;
end Increment;

And usage:

I := 2;
Increment(I);
Put_Line(Positive'Image(I)); -- prints 3
I := 19;
begin
   I := Increment(I); -- Crash, exception on violation of postcondition
exception
   when ASSERT_FAILURE =>
      Put_Line(Positive'Image(I)); -- prints 19
end;
user_26160320

In many cases one can use preconditions and post conditions in leu of in-subprogram validation. On the other hand, sometimes the subprogram must monitor an event or condition repeatedly and then respond properly to the event or condition. In those cases it is often best to perform that monitoring within a subprogram.

user_68544070

The reason I was able to violate my conditions is because I needed to enable assertion of conditions as thindil stated. I solved it by adding

pragma Assertion_Policy (Check);

to my specification file.

user_70616120
Related