Problem 1: Have a Go About It

Consider the following code snippet:

# w is previously defined

x = w
w = w * 2
y = w
w = w * 2
z = w

Use Hoare logic to show that if \(w > 0\) then \(z-y-x > 0\).

Problem 2: Swap Swap Swap

Consider the following code snippet:

x = 0
y = 1
z = x
x = y
y = z

Use Hoare logic to prove that this code snippet swaps the contents of x and y, i.e., x contains 1 and y contains 0 at the end of the snippet.

Problem 3: Reasoning About Conditionals

Next, let’s extend Hoare logic to reason about conditionals. Recall that the form of a conditional statement syntax is:

if <expr>:
    <stmt>
else:
    <stmt>

Suppose that we want some postcondition \(Q\) to be true of the overall conditional. Since it stands to reason that exactly one of the if-branch or else-branch will execute after execution of the conditional, if both branches satisfy the postcondition \(Q\), then we can conclude the overall conditional satisfies \(Q\). The following rule codifies this logic:

{{ P }}
s1
{{ Q }}

{{ P }}
s2
{{ Q }}

{{ P }}
if e:
    s1
else:
    s2
{{ Q }}

With this rule, consider the following code snippet:

# x is previously defined

if x == 0:
    y = 1
else:
    y = 5

Use Hoare logic to prove that \(y > 0\) after the conditional finishes executing.

Problem 4: Upgrading Conditionals

It turns out that our initial rule for conditionals is not strong enough! That is, some precondition-program pairs involving conditionals cannot be proven using that rule. To see this fact, consider the following code snippet:

# x is previously defined

if x == 0:
    y = 2
else:
    y = x + 1

And the postcondition \(x \leq y\).

1. Inspect the code and write down a one-sentence intuitive explanation as to why the postcondition holds of this snippet.

2. Attempt to prove that the postcondition holds with Hoare logic and our current rule for conditionals. In a sentence or two, identify where your proof fails and what is the missing piece of logic from your formal proof.

3. Change the reasoning rule for conditionals with additional conditions when reasoning about the preconditions of the branches so that you can prove the postcondition above.

   (Hint: when you go into each branch, what additional fact do you know is true by virtue of how conditionals work?)