GCD is the "e-coli" of formal methods ... method Gcd(a: int, b: int) returns (r: int) ... but the Dafny versions I have found use a definition for gcd that seems tailored for Euclid's algorithm--rather than the conventional definition. This is
quite correct but I found it unsatisfying so I've written a GCD with a definition of gcd that's very close to the usual one. (I had trouble with existential quantifiers so I avoided them. I am also not a fan of IF ELSE nesting.)
The code uses a technique in which one creates an outline of the proposed algorithm in the form of a sequence of predicates whose conjunction implies the postconditions. This sequence is called an "algorithm plan" and it can be separately verified
(as Rustan has pointed out). The code referenced does that, using:
/ 0 < r <= x
/ CommDivsP1P2EqCommDivsP3P4(r, x, a, b)
/ r >= x
-- where "CSG" stands for "cumulative subgoal" and CSG2 is "common divisors of parameters 1 and 2 equal the common divisors of parameters 3 and 4."
Separate algorithm plan verification is cool but not necessary.
The technique fulfills each subgoal while maintaining all prior subgoals. A fulfillment may require a loop, a recursive call, or whatever. In the case of a loop, its invariants are the prior subgoals.
The code is at http://rise4fun.com/Dafny/IyBA