Merge branch '863-forward-propagation-strategy-accept-optionnal-arguments' into ...
[why3.git] / examples / power.mlw
blob43153710786d9e7968468f6ac3e06166d58a580b
2 (** {1 Fast exponentiation} *)
4 module FastExponentiation
6   use int.Int
7   use int.Power
8   use int.ComputerDivision
10   lemma Power_even:
11     forall x, n. n >= 0 -> mod n 2 = 0 ->
12     power x n = power (x*x) (div n 2)
13       by n = div n 2 + div n 2
15   (* recursive implementation *)
17   let rec fast_exp (x n: int) : int
18     variant  { n }
19     requires { 0 <= n }
20     ensures  { result = power x n }
21   = if n = 0 then
22       1
23     else
24       let r = fast_exp x (div n 2) in
25       if mod n 2 = 0 then r * r else r * r * x
27   (* recursive implementation with an accumulator *)
29   let rec fast_exp_2 (x n acc: int) : int
30     variant  { n }
31     requires { 0 <= n }
32     ensures  { result = power x n * acc }
33   = if n = 0 then
34       acc
35     else if mod n 2 = 0 then
36       fast_exp_2 (x * x) (div n 2) acc
37     else
38       fast_exp_2 x (n - 1) (x * acc)
40   (* non-recursive implementation using a while loop *)
42   use ref.Ref
44   let fast_exp_imperative (x n: int) : int
45     requires { 0 <= n }
46     ensures { result = power x n }
47   = let ref r = 1 in
48     let ref p = x in
49     let ref e = n in
50     while e > 0 do
51       invariant { 0 <= e }
52       invariant { r * power p e = power x n }
53       variant   { e }
54       label L in
55       if mod e 2 = 1 then r := r * p;
56       p := p * p;
57       e := div e 2;
58       assert { power p e = let x = power (p at L) e in x * x }
59     done;
60     r
62 end