examples/gcd_bezout.mlw

   1
   2 (** {1 Greatest common divisor, with Bézout coefficients} *)
   3
   4 module GcdBezout
   5
   6   use int.Int
   7   use int.ComputerDivision
   8   use number.Gcd
   9   use ref.Ref
  10
  11   let gcd (x y: int) : (result: int, ghost a: int, ghost b: int)
  12     requires { x >= 0 /\ y >= 0 }
  13     ensures  { result = gcd x y }
  14     ensures  { a*x + b*y = result }
  15     =
  16     let x = ref x in let y = ref y in
  17     label Pre in
  18     let ghost a = ref 1 in let ghost b = ref 0 in
  19     let ghost c = ref 0 in let ghost d = ref 1 in
  20     while !y > 0 do
  21        invariant { !x >= 0 /\ !y >= 0 }
  22        invariant { gcd !x !y = gcd (!x at Pre) (!y at Pre) }
  23        invariant { !a * (!x at Pre) + !b * (!y at Pre) = !x }
  24        invariant { !c * (!x at Pre) + !d * (!y at Pre) = !y }
  25        variant   { !y }
  26        let r = mod !x !y in let ghost q = div !x !y in
  27        x := !y; y := r;
  28        let ghost ta = !a in let ghost tb = !b in
  29        a := !c; b := !d;
  30        c := ta - !c * q; d := tb - !d * q;
  31     done;
  32     !x, !a, !b
  33
  34 end