Cheap and Secure Web Hosting Provider : See Now

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

, , No Comments
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.

Asked By : Trismegistos

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

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback