Update GCD Example

[DavePearce]

Thanks to Erik Van Wyk for pointing out that you can verify more interesting stuff for the GCD benchmark. Based on his example, I coded up a new implementation here:

function gcd( int m, int n) -> (int r)
requires m >= 1 && n >= 1
//ensures all { j in r+1 .. ?? | m % j != 0 == n % j != 0 }
ensures mod(n,r) == 0 && mod(m,r) == 0:
    //
    int i
    if m > n:
        i = n
    else:
        i = m
    //
    while mod(n,i) != 0 || mod(m,i) != 0
    where i > 0:
        i = i - 1
    //
    return i

// The following function is required because the theorem 
// prover won't reson that r % 1 == 0.  Therefore, I put 
// it in the post-condition explicitly to get around this 
// and use an unsafe assumption.
function mod(int n, int i) -> (int r)
requires i > 0
ensures r != 0 ==> i != 1
ensures i != 1 ==> r == n % i:
    //
    if i == 1:
        assume n % 1 == 0
        return 0
    else:
        return n % i

The need for the mod() function is to do with limitations of the theorem prover's ability to reason about the remainder % operator.