power.mlw 836 Bytes
Newer Older
1

2
(* fast exponentiation *)
3

4
module FastExponentiation
5 6

  use import int.Int
7
  use import int.Power
8 9
  use import int.ComputerDivision

10 11
  (* recursive implementation *)

12 13 14 15
  let rec fast_exp x n variant { n }
    requires { 0 <= n }
    ensures { result = power x n }
  = if n = 0 then
16 17 18 19 20 21
      1
    else begin
      let r = fast_exp x (div n 2) in
      if mod n 2 = 0 then r * r else r * r * x
    end

22 23
  (* non-recursive implementation using a while loop *)

24
  use import ref.Ref
25

26 27 28 29
  let fast_exp_imperative x n
    requires { 0 <= n }
    ensures { result = power x n }
  = let r = ref 1 in
30 31 32
    let p = ref x in
    let e = ref n in
    while !e > 0 do
Andrei Paskevich's avatar
Andrei Paskevich committed
33
      invariant { 0 <= !e /\ !r * power !p !e = power x n }
34
      variant   { !e }
35 36
      if mod !e 2 = 1 then r := !r * !p;
      p := !p * !p;
37
      e := div !e 2
38 39 40 41
    done;
    !r

end