2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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\}$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.