gcc/testsuite/gnat.dg/discr40.ads

   1 pragma Assertion_Policy(Check);
   2
   3 package 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
  26 end Discr40;