后置条件的含义

Question

我可以理解这段代码中前置条件的含义和目的，但在理解后置条件的含义和目的方面遇到问题。我知道Push这部分在推入整数后增加指针（Pointer = Pointer~ +1）。我理解Pop这部分是在弹出整数后减少指针（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;

Answer 1

一般来说，后置条件向用户提出了实现者对所讨论的子程序之后系统（子集）的状态如何的承诺。

这里的具体后置条件似乎解释了堆栈是如何实现的。