0

我可以理解这段代码中前置条件的含义和目的，但我在理解后置条件的含义和目的方面存在问题。在Push我知道这部分在推整数后增加指针（指针=指针~+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;
4

3 回答 3

4

使用后置条件，您必须根据子程序对旧状态的影响来定义新状态。

当后置条件说post Pointer = Pointer~ +1时，表示 的新值Pointer应该是旧值 + 1；ieVariable~表示“Variable进入子程序时的值”。

恐怕我不知道是什么S~[Pointer=>X]意思；也许“的Pointer第一个元素S现在是X”（指定所有其他元素S都保持不变呢？）。

几点：

  • 这是 SPARK2014 符号 ( with SPARK_Mode;) 和旧式注释 ( --#) 的不寻常混合。我想知道新的 SPARK 软件 ( gnatprove) 是否需要第一个才能识别第二个，但它看起来更像是从旧到新转换的中间阶段。
  • Pointer对于显然是数组索引的东西来说，这是一个愚蠢的名字。也许Top会少一些误导。
于 2018-12-05T16:04:36.727 回答
3

通常，后置条件向用户提供了实现者的承诺，即系统（的子集）的状态在相关子程序之后将如何。

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

于 2018-12-05T13:59:49.387 回答
0

另一个高级解释：前置条件是让调用者进入的要求，后置条件是检查内部发生的事情

于 2018-12-06T15:08:37.993 回答