CODEWITHSUNDEEP
adapost-conditionsspark-ada
Memo
Memo

Reputation: 53

The meaning of postcondition

I can understand the meaning and purpose of preconditions in this code but I have a problem in understanding the meaning and purpose of the postconditions. In Push I know that this part to increase pointer after pushing integer ( Pointer = Pointer~ +1 ). In Pop I understand this part to decrease pointer after popping integer (Pointer=Pointer~ - 1).

package Stack

  --# own S, Pointer;
  --# initializes S, Pointer;
   with SPARK_Mode
is
   pragma Elaborate_Body(Stack);  

   Stack_Size       : constant := 100;
   subtype Pointer_Range is Integer range 0 .. Stack_Size;
   subtype Index_Range is Pointer_Range range 1..Stack_Size;
   type Vector is array(Index_Range) of Integer;
   S                : Vector;
   Pointer          : Pointer_Range;

   function isEmpty return Boolean;
   --# global in Pointer;


   procedure Push(X : in Integer);
   --# global in out S, Pointer;
   --# derives S       from S, Pointer, X &
   --#         Pointer from Pointer;


   procedure Pop(X : out Integer);
   --# global in S; in out Pointer;
   --# derives Pointer from Pointer &
   --#         X       from S, Pointer;


   procedure Peek(X : out Integer);
   --# global in S, Pointer;
   --# derives X from S, Pointer;


   procedure Swap(OldLoc, NewLoc: in Pointer_Range);
   --# global in out S;
   --#        in Pointer;
   --# derives S from S, OldLoc, NewLoc, Pointer ;



end Stack;

Upvotes: 0

Views: 1256

Answers (3)

Álex
Álex

Reputation: 1703

Yet another high-level interpretation: preconditions are requirements to let the caller in, postconditions are checks on what happened inside

Upvotes: 0

Simon Wright
Simon Wright

Reputation: 25501

With postconditions, you have to define the new state in terms of the effect the subprogram should have had on the old state.

When the postcondition says post Pointer = Pointer~ +1, it means that the new value of Pointer should be the old value + 1; i.e. Variable~ means "the value of Variable on entry to the subprogram".

I’m afraid I don’t know what S~[Pointer=>X] means; perhaps "the Pointerth element of S is now X" (what about specifying that all the other elements of S are to be unchanged?).

A couple of points:

  • This is an unusual mixture of SPARK2014 notation (with SPARK_Mode;) and old-style annotations (--#). I wondered whether the new SPARK software (gnatprove) needs the first in order to recognise the second, but it looks more like this is an intermediate stage in a conversion from old to new.
  • Pointer is a silly name for something that is clearly an array index. Perhaps Top would be less misleading.

Upvotes: 4

Jacob Sparre Andersen
Jacob Sparre Andersen

Reputation: 6611

In general, a post-condition presents the promises from the implementor to the user of how the state of (a subset of) the system will be after a to the subprogram in question.

The specific post-conditions here seem to explain how the stack is implemented.

Upvotes: 5

Related Questions