Cheap and Secure Web Hosting Provider : See Now

# [Solved]: Why precondition strengtening is sound in Hoare logic

, ,
Problem Detail:

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.

#### Answered By : Yuval Filmus

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