examples/power.mlw

   1
   2 (** {1 Fast exponentiation} *)
   3
   4 module FastExponentiation
   5
   6   use int.Int
   7   use int.Power
   8   use int.ComputerDivision
   9
  10   lemma Power_even:
  11     forall x, n. n >= 0 -> mod n 2 = 0 ->
  12     power x n = power (x*x) (div n 2)
  13       by n = div n 2 + div n 2
  14
  15   (* recursive implementation *)
  16
  17   let rec fast_exp (x n: int) : int
  18     variant  { n }
  19     requires { 0 <= n }
  20     ensures  { result = power x n }
  21   = if n = 0 then
  22       1
  23     else
  24       let r = fast_exp x (div n 2) in
  25       if mod n 2 = 0 then r * r else r * r * x
  26
  27   (* recursive implementation with an accumulator *)
  28
  29   let rec fast_exp_2 (x n acc: int) : int
  30     variant  { n }
  31     requires { 0 <= n }
  32     ensures  { result = power x n * acc }
  33   = if n = 0 then
  34       acc
  35     else if mod n 2 = 0 then
  36       fast_exp_2 (x * x) (div n 2) acc
  37     else
  38       fast_exp_2 x (n - 1) (x * acc)
  39
  40   (* non-recursive implementation using a while loop *)
  41
  42   use ref.Ref
  43
  44   let fast_exp_imperative (x n: int) : int
  45     requires { 0 <= n }
  46     ensures { result = power x n }
  47   = let ref r = 1 in
  48     let ref p = x in
  49     let ref e = n in
  50     while e > 0 do
  51       invariant { 0 <= e }
  52       invariant { r * power p e = power x n }
  53       variant   { e }
  54       label L in
  55       if mod e 2 = 1 then r := r * p;
  56       p := p * p;
  57       e := div e 2;
  58       assert { power p e = let x = power (p at L) e in x * x }
  59     done;
  60     r
  61
  62 end