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

pragma SPARK_Mode(on);

function Fibonacci (N: Natural) return Natural
is
   X : Natural := 0;
   Y : Natural := 1;
   Z : Natural := 1;
begin
   case N is
      when 0 =>
         return 0;
      when 1 =>
         return 1;
      when others =>
         for I in 2 .. N loop
            Z := X + Y;
            pragma Loop_Invariant (X = Fibonacci(I-2)
                                   and Y = Fibonacci(I-1)
                                   and Z = Fibonacci(I));
            X := Y;
            Y := Z;
         end loop;
         return Z;
   end case;
end Fibonacci;