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:
- $\mathtt{Assignment}$
- 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.
- $\mathtt{Sequencing}$
- 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$.
- $\mathtt{Conditionals}$
- "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$"
- This is essentially a sequential composition.
- 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.
- $\mathtt{Iteration}$
- "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.
- 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.
- $\mathtt{Weakening \to Strengthening}$
- I don't understand this one yet.
To summarize, these are my questions:
- 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]\}$
- How to interpret the assignment rule.
- How the while loop is allowed to be an axiom, when it does so much.
Thank you so much for the help.