examples/gcd_vc_sp.mlw

   1
   2 (** Greatest common divisor, using the Euclidean algorithm *)
   3
   4 module EuclideanAlgorithm
   5
   6   use mach.int.Int
   7   use number.Gcd
   8
   9   let rec euclid (u v: int) : int
  10     variant  { v }
  11     requires { u >= 0 /\ v >= 0 }
  12     ensures  { result = gcd u v }
  13   = [@vc:sp]
  14     if v = 0 then
  15       u
  16     else
  17       euclid v (u % v)
  18
  19 end
  20
  21 module EuclideanAlgorithmIterative
  22
  23   use mach.int.Int
  24   use ref.Ref
  25   use number.Gcd
  26
  27   let euclid (u0 v0: int) : int
  28     requires { u0 >= 0 /\ v0 >= 0 }
  29     ensures  { result = gcd u0 v0 }
  30   = [@vc:sp]
  31     let u = ref u0 in
  32     let v = ref v0 in
  33     while !v <> 0 do
  34       invariant { !u >= 0 /\ !v >= 0 }
  35       invariant { gcd !u !v = gcd u0 v0 }
  36       variant   { !v }
  37       let tmp = !v in
  38       v := !u % !v;
  39       u := tmp
  40     done;
  41     !u
  42
  43 end
  44
  45 module BinaryGcd
  46
  47   use mach.int.Int
  48   use number.Parity
  49   use number.Gcd
  50
  51   lemma even1: forall n: int. 0 <= n -> even n <-> n = 2 * div n 2
  52   lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1
  53   lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2
  54
  55   use number.Coprime
  56
  57   lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u ->
  58     gcd (2 * u) (2 * v) = 2 * gcd u v
  59   lemma gcd_even_odd: forall u v: int. 0 <= v -> 0 <= u ->
  60     gcd (2 * u) (2 * v + 1) = gcd u (2 * v + 1)
  61   lemma gcd_even_odd2: forall u v: int. 0 <= v -> 0 <= u ->
  62     even u -> odd v -> gcd u v = gcd (div u 2) v
  63   lemma odd_odd_div2: forall u v: int. 0 <= v -> 0 <= u ->
  64     div ((2*u+1) - (2*v+1)) 2 = u - v
  65
  66   let lemma gcd_odd_odd (u v: int)
  67     requires { 0 <= v <= u }
  68     ensures { gcd (2 * u + 1) (2 * v + 1) = gcd (u - v) (2 * v + 1) }
  69   = assert { gcd (2 * u + 1) (2 * v + 1) =
  70              gcd ((2*u+1) - 1*(2*v+1)) (2 * v + 1) }
  71
  72   lemma gcd_odd_odd2: forall u v: int. 0 <= v <= u ->
  73     odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v
  74
  75   let rec binary_gcd (u v: int) : int
  76     variant  { v, u }
  77     requires { u >= 0 /\ v >= 0 }
  78     ensures  { result = gcd u v }
  79   = [@vc:sp]
  80     if v > u then binary_gcd v u else
  81     if v = 0 then u else
  82     if mod u 2 = 0 then
  83       if mod v 2 = 0 then 2 * binary_gcd (u / 2) (v / 2)
  84                      else binary_gcd (u / 2) v
  85       else
  86       if mod v 2 = 0 then binary_gcd u (v / 2)
  87                      else binary_gcd ((u - v) / 2) v
  88
  89 end
  90
  91 (** With machine integers.
  92     Note that we assume parameters u, v to be nonnegative.
  93     Otherwise, for u = v = min_int, the gcd could not be represented. *)
  94
  95 (* does not work with extraction driver ocaml64
  96 module EuclideanAlgorithm31
  97
  98   use mach.int.Int31
  99   use number.Gcd
 100
 101   let rec euclid (u v: int31) : int31
 102     variant  { to_int v }
 103     requires { u >= 0 /\ v >= 0 }
 104     ensures  { result = gcd u v }
 105   =
 106     if v = 0 then
 107       u
 108     else
 109       euclid v (u % v)
 110
 111 end
 112 *)
 113
 114 module EuclideanAlgorithm63
 115
 116   use mach.int.Int63
 117   use number.Gcd
 118
 119   let rec euclid (u v: int63) : int63
 120     variant  { to_int v }
 121     requires { u >= 0 /\ v >= 0 }
 122     ensures  { result = gcd u v }
 123   = [@vc:sp]
 124     if v = 0 then
 125       u
 126     else
 127       euclid v (u % v)
 128
 129 end