1generic
2package Predicate14 with
3  SPARK_Mode
4is
5
6   type Field_Type is (F_Initial, F_Payload, F_Final);
7
8   type State_Type is (S_Valid, S_Invalid);
9
10   type Cursor_Type (State : State_Type := S_Invalid) is private;
11
12   type Cursors_Type is array (Field_Type) of Cursor_Type;
13
14   type Context_Type is private;
15
16   type Result_Type (Field : Field_Type := F_Initial) is
17      record
18         case Field is
19            when F_Initial | F_Final =>
20               null;
21            when F_Payload =>
22               Value : Integer;
23         end case;
24      end record;
25
26   function Valid_Context (Context : Context_Type) return Boolean;
27
28private
29
30   function Valid_Type (Result : Result_Type) return Boolean is
31     (Result.Field = F_Initial);
32
33   type Cursor_Type (State : State_Type := S_Invalid) is
34      record
35         case State is
36            when S_Valid =>
37               Value : Result_Type;
38            when S_Invalid =>
39               null;
40         end case;
41      end record
42      with Dynamic_Predicate =>
43          (if State = S_Valid then Valid_Type (Value));
44
45   type Context_Type is
46      record
47         Field : Field_Type := F_Initial;
48         Cursors : Cursors_Type := (others => (State => S_Invalid));
49      end record;
50
51   function Valid_Context (Context : Context_Type) return Boolean is
52     (for all F in Context.Cursors'Range =>
53         (Context.Cursors (F).Value.Field = F));
54
55   procedure Dummy;
56end Predicate14;