1package SPARK2 with SPARK_Mode is
2
3   function Expon (Value, Exp : Natural) return Natural is
4      (if Exp = 0 then 1
5       else Value * Expon (Value, Exp - 1))
6   with Ghost,
7        Pre => Value <= Max_Factorial_Number and Exp <= Max_Factorial_Number,
8        Annotate => (GNATprove, Terminating);  --  CRASH!
9
10   Max_Factorial_Number : constant := 6;
11
12   function Factorial (N : Natural) return Natural with
13      Pre => N < Max_Factorial_Number,
14      Post => Factorial'Result <= Expon (Max_Factorial_Number, N);
15
16end SPARK2;
17