## Greatest common divisor with Bezout coefficients

**Authors:** Jean-Christophe Filliâtre

**Topics:** Mathematics / Ghost code

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

# Greatest common divisor, with Bézout coefficients

module GcdBezout use import int.Int use import int.ComputerDivision use import number.Gcd use import ref.Ref let gcd (x:int) (y:int) requires { x >= 0 /\ y >= 0 } ensures { result = gcd x y } ensures { exists a b:int. a*x+b*y = result } = let x = ref x in let y = ref y in 'Pre: let ghost a = ref 1 in let ghost b = ref 0 in let ghost c = ref 0 in let ghost d = ref 1 in while (!y > 0) do invariant { !x >= 0 /\ !y >= 0 } invariant { gcd !x !y = gcd (at !x 'Pre) (at !y 'Pre) } invariant { !a * (at !x 'Pre) + !b * (at !y 'Pre) = !x } invariant { !c * (at !x 'Pre) + !d * (at !y 'Pre) = !y } variant { !y } let r = mod !x !y in let ghost q = div !x !y in assert { r = !x - q * !y }; x := !y; y := r; let ghost ta = !a in let ghost tb = !b in a := !c; b := !d; c := ta - !c * q; d := tb - !d * q; done; !x end

download ZIP archive