(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (* {2 GCD, Bezout coefficients} *) use int.Int use int.ComputerDivision use number.Gcd let gcd (x:int) (y:int) requires { x >= 0 /\ y >= 0 } ensures { result = gcd x y } ensures { exists a,b. result = a*x+b*y } = let ref x = x in let ref y = y in label Init in let ghost ref a = 1 in let ghost ref b = 0 in let ghost ref c = 0 in let ghost ref d = 1 in while y > 0 do invariant { x >= 0 /\ y >= 0 } invariant { gcd x y = gcd (x at Init) (y at Init) } invariant { x = a * (x at Init) + b * (y at Init) } invariant { y = c * (x at Init) + d * (y at Init) } variant { y } let r = mod x y in let ghost q = div x y in (* x = q * y + r *) x <- y; y <- r; let a' = a in let b' = b in a <- c; b <- d; c <- a' - q * c; d <- b' - q * d; done; x (* Local Variables: compile-command: "why3 ide exo_bezout.mlw" End: *)