Mercurial > hg > CbC > CbC_gcc
view gcc/testsuite/gnat.dg/discr40.ads @ 158:494b0b89df80 default tip
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 25 May 2020 18:13:55 +0900 |
parents | 04ced10e8804 |
children |
line wrap: on
line source
pragma Assertion_Policy(Check); package Discr40 is subtype Element is Integer; type Vector is array (Positive range <>) of Element; type Stack (Max_Length : Natural) is record Length : Natural; Data : Vector (1 .. Max_Length); end record; function Not_Full (S : Stack) return Boolean is (S.Length < S.Max_Length); procedure Push (S: in out Stack; E : Element) with Pre => Not_Full(S), -- Precodition Post => -- Postcondition (S.Length = S'Old.Length + 1) and (S.Data (S.Length) = E) and (for all J in 1 .. S'Old.Length => S.Data(J) = S'Old.Data(J)); end Discr40;