Description
Greatest Common Divisor
All the references to gcd in this hand out are related to Euclid’s algorithm as discussed in class with the
relevant material already posted on the course webpage. In math mode, we use the standard notation
(a, b)
(from number theory) to refer to the greatest common divisor of a and b.
Problem 1 (10 points)
Prove that the Euclid’s algorithm for computing the gcd satisfies the following:
∀a, b, m ∈ N : (a, b) = (mb − a, b) if mb > a
∀a, b, m ∈ N : (a, b) = (a − mb, b) if mb < a
by giving a proof for the following lemma in Dafny:
lemma SubCancelation(a: nat, b: nat, m: nat)
requires a > 0 && b > 0
ensures m * b > a ==> gcd(m * b – a, b) == gcd(a,b)
ensures m * b < a ==> gcd(a – m * b, b) == gcd(a,b)
You may not change the signature of the above lemma. Only provide a body for it which proves it correct.
Problem 2 (45 points)
Consider the predicate divides as defined below:
predicate divides(a: nat, b:nat)
requires a > 0
{
exists k: nat :: b == k * a
}
It formalizes the standard mathematical concept of a|b.
(a) (25 points) Encode the following property of gcd in Dafny and prove it:
∀k, a, b ∈ N : k|a ∧ k|b =⇒ k|(a, b)
Note that we want to prove that Euclid’s GCD algorithm satisfies the above (and not the mathematical
definition of (a, b).
(b) (30 points) Prove that gcd is associative, that is:
∀a, b, c ∈ N : (a,(b, c)) = ((a, b), c)
Part (a) may help with one way of arguing for this, but any other proof unrelated to part (a) will be
equally fine.
2
