Wiki Agenda Contact Version française

Fast exponentiation

Two different implementations of the logarithmic fast exponentiation algorithm.


Authors: Jean-Christophe Filliâtre / Claude Marché

Topics: Non-linear Arithmetic

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(* fast exponentiation *)

module FastExponentiation

  use import int.Int
  use import int.Power
  use import int.ComputerDivision

  (* recursive implementation *)

  let rec fast_exp x n variant { n }
    requires { 0 <= n }
    ensures { result = power x n }
  = 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 *)

  use import ref.Ref

  let fast_exp_imperative x n
    requires { 0 <= n }
    ensures { result = power x n }
  = 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 }
      if mod !e 2 = 1 then r := !r * !p;
      p := !p * !p;
      e := div !e 2
    done;
    !r

end

download ZIP archive