-- 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;