## 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 int.Int use int.Power use 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 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 } 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

download ZIP archive