patternMinor
Why precondition strengtening is sound in Hoare logic
Viewed 0 times
strengteningwhylogicsoundhoareprecondition
Problem
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.
$$
{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.
Solution
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\}$.
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\}$.
Context
StackExchange Computer Science Q#45543, answer score: 3
Revisions (0)
No revisions yet.