ada - 事後条件の意味

Question

このコードの事前条件の意味と目的は理解できますが、事後条件の意味と目的を理解するのに問題があります。このPush部分は、整数をプッシュした後にポインタを増やすことを知っています（ Pointer = Pointer~ +1 ）。このPop部分は、整数をポップした後にポインターを減らすことを理解しています（ポインター=ポインター〜-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;