gnatprove_13.2.1_28fc3583/share/examples/spark/gnatprove_by_example/ug__functional_imported/functional_imported.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
with System.Storage_Elements;

package body Functional_Imported with
  SPARK_Mode,
  Refined_State => (Max_And_Snd => (Max, Snd))
is
   Max : Natural := 0  --  max value seen
     with Address  => System.Storage_Elements.To_Address (16#8000_0000#),
          Warnings => Off;

   Snd : Natural := 0  --  second max value seen
     with Address  => System.Storage_Elements.To_Address (16#8000_0004#),
          Warnings => Off;

   function Invariant return Boolean is
     (if Max = 0 then Snd = 0 else Snd < Max);

   function Max_Value_Seen return Integer is (Max);

   function Second_Max_Value_Seen return Integer is (Snd);

   procedure Update (X : Natural) with
     Import,
     Convention => C,
     Global => (In_Out => (Max, Snd)),
     Annotate => (GNATprove, Always_Return),
     Pre  => X > Snd and then      --  support of maintenance
             Invariant,            --  invariant checking
     Post => Invariant and then    --  invariant checking
             (if X > Max'Old then  --  complete functional
                Snd = Max'Old and Max = X
              elsif X < Max'Old then
                Snd = X and Max = Max'Old
              else
                Snd = Snd'Old and Max = Max'Old);

   procedure Seen_Two (X, Y : Natural) is
   begin
      if X > Max then
         Max := Y;
         Snd := X;
      elsif X > Snd then
         Update (Y);
         Seen_One (X);
      else
         Seen_One (Y);
      end if;
   end Seen_Two;

end Functional_Imported;