program_proofs_in_spark_0.1.1_37500dca/ch12/fibonacci_squared.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
with Ada.Numerics.Big_Numbers.Big_Integers; use Ada.Numerics.Big_Numbers.Big_Integers;

package Fibonacci_Squared is

   function Fib (N : Big_Natural) return Big_Natural is
      (if N < 2 then N else Fib (N-1) + Fib (N-2))
   with
     Annotate => (GNATprove, Terminating),
     Annotate => (GNATprove, False_Positive, "terminating annotation",
                  "That version of SPARK does not allow variant on Big_Natural");

   function Square_Fib (N : Big_Natural) return Big_Natural
   with
     Post => Square_Fib'Result = Fib (N) * Fib (N);

end Fibonacci_Squared;