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;