(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 Fast exponentiation} *) use int.Int use int.ComputerDivision let rec function power (x:int) (n:int) : int requires { n >= 0 } variant { n } = if n = 0 then 1 else x * power x (n-1) (** a few helper lemmas *) lemma power_mult : forall x y n:int. n >= 0 -> power (x*y) n = power x n * power y n lemma power_even: forall x:int, n:int. n >= 0 /\ mod n 2 = 0 -> power x n = (power (x * x) (div n 2)) lemma power_odd: forall x:int, n:int. n >= 0 /\ mod n 2 = 1 -> power x n = x * (power (x * x) (div n 2)) (** fast exponentiation *) let power_x_n (x:int) (n:int) : int requires { n >= 0 } ensures { result = power x n } diverges = let ref r = 1 in let ref p = x in let ref e = n in while e > 0 do invariant { 0 <= e } invariant { r * power p e = power x n } if mod e 2 = 1 then r <- r * p; p <- p * p; e <- div e 2 done; r