# Feedback on Hoare Logic Test

All the material for this test is available from the [lecture](https://hackmd.io/@m5rnD-8SSPuuSHTKgXvMjg/Hy135C2tH) and the [exercises](https://hackmd.io/@m5rnD-8SSPuuSHTKgXvMjg/rkhVZNzjH).

I first discuss some general tips and then the solutions of the test.

## General Tips

### Learn the Rules of Hoare Logic

The rules are [summarised here](https://hackmd.io/@m5rnD-8SSPuuSHTKgXvMjg/BJyjAXGoB).

Learning the rules gives you easy points.

Knowing the rules helps with the other questions.

### Finding preconditions and postconditions

The postcondition should answer the question: What does the program compute?

If a variable such as $x$ appears more than once in your postcondition check again. For example, $x=x*p$ can only be true if $p=1$ or $x=0$. Is this likely to be the intended result of a while loop?

If $i$ is the variable that is counted down in a loop and you know that upon exiting the loop $i=0$, then this is a postcondition that does not tell you much of interest about the loop. The purpose of the loop is unlikely to be counting down $i$ to $0$.

If $n$ does not appear in the code and you write a postcondition such as $x=p^n$ then you need to say what $n$ refers to ... one way of doing this is to have a precondition such as $x=n$, which says that $n$ is the value of $x$ before the computation.

Preconditions should also contain other conditions which are needed for the code to produce sensible results.

### Finding an invariant

The variables in the body of the loop are usually needed in the invariant. If $x$ and $i$ are variables in the body of the loop and they do not appear in your invariant, check again.

If a variable such as $x$ appears more than once check again. For example, $x=x*i$ can only be true if $i=1$ or $x=0$.

It can be useful to make a table with a sample execution, to see how the variables change during the execution of the loop. Make sure that the table actually corresponds to an execution. Check your invariant against this data.

Finding an invariant just from reading the code can be difficult. The way to find an invariant, is to first understand what the code is (supposed to be) doing.

### Proving an invariant correct

If the body of the loop is just a sequence of assignments, then you only need to check that pulling back the invariant-as-a-postcondition along the assignments gives you the invariant-as-a-precondition.

I don't see how a table could help with this kind of problem.

### Proving pre/postconditions from the invariant

You need to show that
- the precondition implies the invariant
- the invariant and the negated test of the while-loop imply the postcondition

(If you wonder which rule of Hoare logic, in addition to the while-rule, justifies this reasoning step: It is the weakening rule.)

I don't see how a table could help with this kind of problem.

### Self Test

Correct the following statement.

"The invariant needs to hold before and after." [^beforeandafter]
[^beforeandafter]: If the invariant holds before, then it needs to hold after. Note that this does **not** say that the invariant needs to hold before.

## Solution to the Test

### Question 1

See the [summary of rules](https://hackmd.io/@m5rnD-8SSPuuSHTKgXvMjg/BJyjAXGoB).

### Question 2

The post condition should be the result of the computation. For example, in this case $$x=p^{n+1}$$

The precondition records the requirements under which this result will be obtained. In this case $$i=n \wedge x=1$$

The invariant must involve the variables that change in the loop, here $x$ and $i$. In our case the following works
$$x=p^{n-i}$$
To find the postcondition and the invariant, or to **test** whether this formula is correct, a table can help. If we start with $i=n$ and $x=1$, then the formula is correct before the loop because $p^0=1$. After the loop, it still holds because $p^{n-(n-1)}=p$ which also is $x$. This shows that the table does not contradict $x=p^{n-i}$ being an invariant. It is also not difficult to use the techniques of the next question to prove that $x=p^{n-i}$ is indeed an invariant.

In any case there is an important difference in testing a formula and in proving it correct. Testing covers only finitely many executions, correctness proofs account for all infinitely many possible executions. How to do this is the purpose of the next question.

### Question 3

#### 3a

To show that $$x=\frac{n!}{i!}$$ is an invariant, we only have to apply the assignment rule twice.

The first time, for $i:=i-1$ we get from $x=\frac{n!}{i!}$ the precondition $x=\frac{n!}{(i-1)!}$. Then we pull that condition back along $x:=x*i$ which gives the precondition $x*i=\frac{n!}{(i-1)!}$. Dividing both sides by $i$ yields $x=\frac{n!}{i!}$, showing that the $x=\frac{n!}{i!}$ is indeed an invariant.

To show that $$i\ge 0$$ is an invariant, we do the same. Pulling back along $i:=i-1$ gives the condition $i-1\ge 0$ and pulling back along $x:=x*i$ does not change this condition. Now we see that $i-1\ge 0$ is equivalent to $i>0$, which is the test of the while loop.

To summarise, we have shown $\{I\wedge B\}S\{I\}$, where $S$ is the body of the loop, $I$ is the invariant and $B$ is the test of the loop.

#### 3b

For the **precondition**, we need to show [^precondition]
[^precondition]: More formally, we need to show $P\Rightarrow I$ where $I$ is the invariant and $P$ is the precondition.

$$i=n \wedge x=1 \ \ \Rightarrow \ \ x=\frac{n!}{i!}$$

which is immediate. We also need that

$$i=n \wedge x=1 \ \ \Rightarrow \ \ i\ge 0$$

for which we need to assume that $n\ge 0$.

For the **postcondition**, we need to show [^postcondition]
[^postcondition]: More formally, we need to show $I\wedge \neg B\Rightarrow Q$ where $I$ is the invariant, $B$ is the test of the while-loop and $Q$ is the postcondition.

$$i\ge 0 \wedge \neg(i>0) \wedge x=\frac{n!}{i!}\ \ \Rightarrow \ \ x=n!$$

which follows from $i=0$ and $0!=1$.