power_vc_sp.mlw 934 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5

(* fast exponentiation *)

module FastExponentiation

6 7 8
  use int.Int
  use int.Power
  use int.ComputerDivision
MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12 13 14

  (* recursive implementation *)

  let rec fast_exp x n variant { n }
    requires { 0 <= n }
    ensures { result = power x n }
15
  = [@vc:sp]
MARCHE Claude's avatar
MARCHE Claude committed
16 17 18 19 20 21 22 23 24
    if n = 0 then
      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

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

25
  use ref.Ref
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28 29

  let fast_exp_imperative x n
    requires { 0 <= n }
    ensures { result = power x n }
30
  = [@vc:sp]
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
    let r = ref 1 in
    let p = ref x in
    let e = ref n in
    while !e > 0 do
      invariant { 0 <= !e /\ !r * power !p !e = power x n }
      variant   { !e }
      label L in
      if mod !e 2 = 1 then r := !r * !p;
      p := !p * !p;
      e := div !e 2;
      assert { power !p !e =
               let x = power (!p at L) !e in x * x }
    done;
    !r

end