Значение постусловия - PullRequest
Новая
       13

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

0 голосов
/ 05 декабря 2018

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

0 голосов
/ 05 декабря 2018

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

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

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

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

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

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

0 голосов
/ 05 декабря 2018

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

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

...