gcd_bezout.mlw 980 Bytes
Newer Older
1

2
(** {1 Greatest common divisor, with Bézout coefficients} *)
3 4

module GcdBezout
5

6 7 8 9
  use int.Int
  use int.ComputerDivision
  use number.Gcd
  use ref.Ref
MARCHE Claude's avatar
MARCHE Claude committed
10

11
  let gcd (x y: int) : (result: int, ghost a: int, ghost b: int)
12 13
    requires { x >= 0 /\ y >= 0 }
    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 19
    let ghost a = ref 1 in let ghost b = ref 0 in
    let ghost c = ref 0 in let ghost d = ref 1 in
20
    while !y > 0 do
21
       invariant { !x >= 0 /\ !y >= 0 }
22 23 24
       invariant { gcd !x !y = gcd (!x at Pre) (!y at Pre) }
       invariant { !a * (!x at Pre) + !b * (!y at Pre) = !x }
       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
MARCHE Claude's avatar
MARCHE Claude committed
33

34
end