## 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 } 'L: if mod !e 2 = 1 then r := !r * !p; p := !p * !p; e := div !e 2; assert { power !p !e = let x = power (at !p 'L) !e in x * x } done; !r end

download ZIP archive