---
# System prepended metadata

title: SSE HW 12

---

# 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
![](https://i.imgur.com/L9PxEjz.png)

# 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$ }

![](https://i.imgur.com/gKwk8px.png)

{ $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

![](https://i.imgur.com/iKpzsLd.png)


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 }
![](https://i.imgur.com/B523f5i.png)
{ 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}

![](https://i.imgur.com/v5rD4z6.png)
![](https://i.imgur.com/pKrbIG0.png)

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


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