program_proofs_in_spark_0.1.1_37500dca/ch5/mult_commutative.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
-- 5.6 Example: Associativity of Multiplication

with Ada.Numerics.Big_Numbers.Big_Integers; use Ada.Numerics.Big_Numbers.Big_Integers;

package Mult_Commutative is

   function Big (X : Integer) return Big_Integer renames To_Big_Integer;

   function Mult (X, Y : Big_Natural) return Big_Natural is
     (if Y = Big (0) then Big (0) else X + Mult (X, Y-1))
   with
     Annotate => (GNATprove, Terminating),
     Annotate => (GNATprove, False_Positive, "terminating annotation",
                  "That version of SPARK does not allow variant on Big_Natural");

   procedure Lemma_Mult_Commutative (X, Y : Big_Natural)
   with
     Ghost,
     Post => Mult (X, Y) = Mult (Y, X);

end Mult_Commutative;