Значение постусловия

Я могу понять значение и цель предварительных условий в этом коде, но у меня есть проблема в понимании значения и цели постусловий. В 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;
Источник

3 ответа

В общем, постусловие представляет обещания от разработчика пользователю о том, каким будет состояние (подмножество) системы после a для рассматриваемой подпрограммы.

Кажется, что конкретные постусловия объясняют, как реализован стек.

Источник

В постусловиях вы должны определить новое состояние с точки зрения влияния подпрограммы на старое состояние.

Когда постусловие говорит post Pointer = Pointer~ +1, это означает, что новое значение Pointer должно быть старое значение + 1; т.е. Variable~ означает "ценность Variable на вход в подпрограмму ".

Боюсь я не знаю что S~[Pointer=>X] средства; возможно " Pointerй элемент S сейчас X" (как насчет указания, что все остальные элементы S должны быть неизменными?).

Пара моментов:

  • Это необычная смесь обозначений SPARK2014 (with SPARK_Mode;) и аннотации в старом стиле (--#). Интересно, будет ли новый SPARK софт (gnatprove) требуется первое, чтобы распознать второе, но похоже, что это промежуточный этап перехода от старого к новому.
  • Pointer глупое имя для чего-то, что явно является индексом массива. возможно Top будет меньше вводить в заблуждение.
Источник

Еще одна интерпретация высокого уровня: предварительные условия - это требования, чтобы позволить вызывающему абоненту, постусловия - это проверка того, что произошло внутри

Источник
Другие вопросы по тегам