1pragma Assertion_Policy(Check);
2
3package Discr40 is
4
5   subtype Element is Integer;
6
7   type Vector is array (Positive range <>) of Element;
8
9   type Stack (Max_Length : Natural) is
10   record
11      Length : Natural;
12      Data : Vector (1 .. Max_Length);
13   end record;
14
15   function Not_Full (S : Stack) return Boolean is
16      (S.Length < S.Max_Length);
17
18    procedure Push (S: in out Stack; E : Element)
19         with Pre => Not_Full(S),   -- Precodition
20              Post =>             -- Postcondition
21                 (S.Length = S'Old.Length + 1) and
22                 (S.Data (S.Length) = E) and
23                 (for all J in 1 .. S'Old.Length =>
24                     S.Data(J) = S'Old.Data(J));
25
26end Discr40;
27