Description
CSC410
Assignment 1
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.
