Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I have problem with understanding why precondition strengthening is sound rule in Hoare logic. The rule is:
$$ {P \implies Q, \{Q\} C \{X\} } \over {\{P\} C \{X\}} $$
I really do not understand why precondition in consequence goes in reverse direction that implication works (modus ponens).
I can understand why post-condition weakening works because it follows modus ponens rule but I am no able to understand precondition strengthening.
The triple $\{Q\}C\{X\}$ states that if $Q$ holds, then after executing $C$, the condition $X$ holds. Now suppose that $\{Q\}C\{X\}$ and that $P \Longrightarrow Q$. We will prove that $\{P\}C\{X\}$. Indeed, suppose that $P$ holds. Since $P \Longrightarrow Q$, also $Q$ holds. Hence if we execute $C$, then $X$ will hold. Altogether, we see that $\{P\}C\{X\}$ is valid.
An example can also be helpful. If we know that $\{x=1\}x\gets x+1\{x=2\}$ then we certainly know that $\{x=y=1\}x\gets x+1\{x=2\}$.
