Я могу понять значение и назначение предварительных условий в этом коде, но у меня есть проблема с пониманием значения и назначения постусловий. В 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;
Stack.Pointer
, не используя ни одну из указанных подпрограмм? - person Jacob Sparre Andersen   schedule 05.12.2018