Wiki Agenda Contact Version française

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