examples/gcd_bezout_vc_sp.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:int) (y:int)
  12     requires { x >= 0 /\ y >= 0 }
  13     ensures  { result = gcd x y }
  14     ensures  { exists a b:int. a*x+b*y = result }
  15   = [@vc:sp]
  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        assert { r = !x - q * !y };
  28        x := !y; y := r;
  29        let ghost ta = !a in let ghost tb = !b in
  30        a := !c; b := !d;
  31        c := ta - !c * q; d := tb - !d * q;
  32     done;
  33     !x
  34
  35 end