Understanding Hoare Logic Axioms

Question

Given these 5 axioms of Hoare Logic:

\begin{array}{cl} \frac{}{\{\phi([x \leftarrow E])\}\ x := E\ \{\phi(x)\}} & \mathtt{Assignment}\\\\ \frac{\{\phi\}\ P_1\ \{\eta\} \quad \{\eta\}\ P_2\ \{\psi\}}{\{\phi\}\ P_1; P_2\ \{\psi\}} & \mathtt{Sequencing}\\\\ \frac{\{\phi \land B\}\ P_1\ \{\psi\} \quad \{\phi \land \neg B\}\ P_2\ \{\psi\}}{\{\phi\}\ \mathtt{if}\ B\ \mathtt{then}\ P_1\ \mathtt{else}\ P_2\ \{\psi\}} & \mathtt{Conditionals}\\\\ \frac{\{\phi \land B\}\ P\ \{\psi\}}{\{\phi\}\ \mathtt{while}\ B\ P\ \{\psi \land \neg B\}} & \mathtt{Iteration}\\\\ \frac{\phi ⇒ \phi1 \quad \{\phi1\}\ P\ \{\psi1\} \quad \psi1 ⇒ \psi}{\{\phi\}\ P\ \{\psi\}} & \mathtt{Weakening \to Strengthening} \end{array}

Trying to understand the following:

1. $\mathtt{Assignment}$
   1. What $\phi([x \leftarrow E])$ means. In the presentation it says $\phi([x \leftarrow E])$ replaces every "free occurence" of $x$ in $\phi$ by $E$. I am confused because I thought that was what the assignment $x := E$ was doing. So my reading is: "precondition: replace each free occurrence of $x$ in state $\phi$ with $E$, program: assign $x$ to $E$, postcondition: $x \in \phi$". I am confused by both the pre and post conditions. To me it should be written $\{\phi[x] \land \phi[E]\}\ x := E\ \{\phi[x == E]\}$, that is, "given $x$ in state $\phi$ and $E$ in state $\phi$, when I assign $x$ to $E$, I get the new state where $x$ is equal to $E$". Wondering if someone could help clarify this my interpretation.
2. $\mathtt{Sequencing}$
   1. This one makes sense. If program $P_1$ leads state $\phi$ to state $\eta$, and program $P_2$ leads state $\eta$ to state $\psi$, then program $P_3 := P_1 ; P_2$ leads state $\phi$ to state $\psi$.
3. $\mathtt{Conditionals}$
   1. "If we're in state $\phi$ and we have variable $B$, then program $P_1$ leads to state $\psi$. Similarly for $P_2$, but when we don't have $B$ in state $\phi$"
   2. This is essentially a sequential composition.
   3. I would've written it as $\{\phi[B]\}\ P_1\ \{\psi\}$ and $\{\phi[\neg B]\}\ P_1\ \{\psi\}$, would be helpful to better understand the notation on why they wrote it with the $\land$. To me $\{\phi \land B\}$ says either "B is true in $\phi$ state" or "B exists in $\phi$ state", can't tell.
4. $\mathtt{Iteration}$
   1. "If $B$ is in state $\phi$, and program $P$ leads to state $\psi$, then $\mathtt{while}\ B\ P$ leads to state $\psi$ without $B$". So this is an axiom.
   2. I don't understand how this can be an axiom because there is so much that is going on (tons of iterations for example). Wondering what allows this to be an axiom.
5. $\mathtt{Weakening \to Strengthening}$
   1. I don't understand this one yet.

To summarize, these are my questions:

1. What the notation is for having certain values in a state in the pre- or post-condition. If it's $\{\phi[B]\}$ or $\{\phi(x \leftarrow B)\}$ or $\{\phi \land B\}$ or $\{\phi(B)\}$. What the preferred notation is and its meaning. I have also seen $\{\phi[B/x]\}$
2. How to interpret the assignment rule.
3. How the while loop is allowed to be an axiom, when it does so much.

Thank you so much for the help.

Answer 1

Here are some answers and hints to pursue your reflexions.

1. $\mathtt{Assignment}$
   1. What $\phi([x \leftarrow E])$ means. You said yourself that the semantic of the precondition confuses you that was what the assignment $x := E$ was doing. But in fact your are precisely pointing out the crux of this rule: it affects the precondition exactly as the assignment would do it. This is the core reason of why this rule is actually sound.

Let study an exemple and leave the abstraction for a bit. Take the program $P = (z:=x+1)$.

Suppose we want to prove the postcondition $\phi(z) := \{z=2\}$ Intuitively what do we need to prove this ? Obviously we need $x$ to be equal to $1$. Let see how it translates in Hoare's logic. The assignment rule tells us that the triple: $$ \{\phi[z \gets x+1]\} (z:=x+1) \{\phi(z)\} $$ is valid.

Unrolling the syntax gives: $$ \{(z=2)[z \gets x+1] \} (z:=x+1) \{x=2\}, $$ that is $$ \{x+1 = 2 \} (z:=x+1) \{z=2\}, $$ and a bit of meta-logic says: $$ \{x = 1 \} (z:=x+1) \{z=2\}. $$

Which is what you wanted.

In an nutshell the assignment intuitively says: "The postcondition is true as soon as when I replace everything by the value of E in it, it is true"

$\mathtt{Conditionals}$

First of all $B$ is not a variable but a boolean predicate (like $X==1$ for instance).

1. $\{\phi[B]\}\ P_1\ \{\psi\}$ doesn't make any sense. $\phi$ is a predicate, so does $B$, so that you can't apply one to another. For instance if $\phi = (x==1), B = (y==2)$ you can speak of $\phi\wedge B$ but $\phi[B] has absolutely no meaning.

2. $\{\phi \land B\}$ is true says $\phi$ is true and $B$ is true. With my previous instances: $\{\phi \land B\}$ as precondition asserts that on the one hand $(x==1)$, and on the other $(y==2)$. Nothing else.

$\mathtt{Iteration}$ This one is subtle. As long as it terminates, you can have arbitrary many iterations BUT still a finite number. Think of a while as a for loop on which you don't know a priori the number of runs in this case. To see why the rule is sound, think of it as a nested sequence of if :

if B then 
     P
     if B then 
         if B then 
            P
            if B then
                 .....

And use a recurrence + conditional+ composition to convince you that the rule does what it is supposed to do.

If it doesn't terminates you can't say anything a priori so it doesn't matter. Remark that the rule DOES NOT say that the loop terminates.

$\mathtt{Weakening \to Strengthening}$ It is the causal reasoning. Let us unroll the rule: Suppose that $\phi$ is true. Then $\phi$ is also true since $\phi \Rightarrow \phi_1$. But the Hoare triple $\{\phi_1\}\ P_1\ \{\psi_1\}$ is valid by hypothesis. Then $\psi_1$ is true. But we know that $\psi_1\Rightarrow \psi$. Hence $\psi$ is true as well: we just proved that $\{ \phi \} P \{\psi\}$ is a valid triple.