# SSE HW 12

# 1

- False, assuming that the program is run in python (does not terminate)
- True, the precondition is not met in the first place so it doesn't matter. This however is a valid Hoare Triple
- True

# 2

# 3

{$K > 0$ and $M > 0$ && $k == K$ && $m == M$}

while(k!=m) {
    if (k > m) {k = k - m;}
    else {m = m - k;}
    }
return k;

{the returned value is GCD of the inputs}

The invariant would be:

$𝐾 ≥ 𝑘$ 𝑎nd $𝑀 ≥ 𝑚$ && $𝑔cd(𝐾,𝑀) == 𝑔cd(𝑘,𝑚)$

1) [x] pre ⇒ inv:
- {$K > 0$ and $M > 0$ && $k == K$ && $m == M$} ⇒ $𝐾 ≥ 𝑘$ 𝑎nd $𝑀 ≥ 𝑚$ && $𝑔cd(𝐾,𝑀) == 𝑔cd(𝑘,𝑚)$
- This property is satisfied.

2) [x] { inv && b } program { inv }:

{$𝐾 ≥ 𝑘$ 𝑎nd $𝑀 ≥ 𝑚$ && $𝑔cd(𝐾,𝑀) == 𝑔cd(𝑘,𝑚)$ && $k != m$}

if (k > m) {k = k - m;}
else {m = m - k;}

{$𝐾 ≥ 𝑘$ 𝑎nd $𝑀 ≥ 𝑚$ && $𝑔cd(𝐾,𝑀) == 𝑔cd(𝑘,𝑚)$}

- k > m ⇒ (m = oldm - k) || m > k ⇒ (k = oldk – m) && oldk != oldm && gcd(K,M) == gcd(k,m) && oldk = K && oldm = M (from the precondition)
- k > m ⇒ gcd(K, M) == gcd(oldk – m, m) || m > k ⇒ gcd(K,M) == gcd(k, oldm– k)
- k > m ⇒ gcd(K, M) == gcd(K – m, m) || m > k ⇒ gcd(K,M) == gcd(k, M – k)
- { K ≥ k and M ≥ m && gcd(K,M) == gcd(k,m) }

> This property is satisfied as it follows Euclidean’s principle that gcd(A,B) = gcd(A-B, B).

3) [x] inv && !b ⇒ post:
{$𝐾 ≥ 𝑘$ 𝑎nd $𝑀 ≥ 𝑚$ && $𝑔cd(𝐾,𝑀) == 𝑔cd(𝑘,𝑚)$ && $k == m$}

- K ≥ k and M ≥ k && gcd(K,M) == gcd(k,k)
- K ≥ k and M ≥ k && gcd(K,M) == k
- {the returned value is GCD of the inputs}

> The invariant and !b are strong enough to imply the postcondition.

Thus, as all three rules are satisfied, the program has partial correctness.

# 4

The program will halt when k == m.

We can use f(k,m) = k + m as a ranking function to test whether the program terminates.

{ $k + m = V$ }


{ $k + m = V’$ && $V’ < V$ }

The Hoare triple is true after iterations of the while loop as the rank decreases after each loop.
- When k is greater than m, the value of k decreases by m. $f(k,m) = k$
- When m is greater than k, the value of m decreases by k. $f(k,m) = m$

Thus eventually, k and m will converge to the same value, and the program has total correctness.

# 5


The program has 2 loops (`while (x>=0)` and `while (y <x)` ) as such 2 checks are needed to check for termination

### `while (y <x)` loop
Assuming that x is ≥ 0, using the ranking function $f(y)=-y$

{ x-y = V }
{ x-y = V’ && V’ < V }
> This loop reaches termination

### `while (x>=0)` loop
Assuming no integer overflow and x > 0, using the ranking function $f(x)=x$

{x = V}


{ x = V’ && V’ < V }
> This loop reaches termination

As both loops reach termination, ther program will always reach termination and has total correctness.