# Problem 1: Have a Go About It

Consider the following Python code snippet:

```
# w is previously defined
= w
x = w * 2
w = w
y = w * 2
w = w z
```

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

# Problem 2: Swap Swap Swap

Consider the following Python code snippet:

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

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 in Python 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:

**Rule (Conditional)**: If

```
{{ P }}
s1 {{ Q }}
```

and

```
{{ P }}
s2 {{ Q }}
```

for statements `s1`

and `s2`

. Then we can
conclude:

```
{{ P }}if e:
s1else:
s2 {{ Q }}
```

With this rule, consider the following code snippet:

```
# x is previously defined
if x == 0:
= 1
y else:
= 5 y
```

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:
= 2
y else:
= x + 1 y
```

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

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

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.

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?)