HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Why precondition strengtening is sound in Hoare logic

Submitted by: @import:stackexchange-cs··
0
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.

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

Context

StackExchange Computer Science Q#45543, answer score: 3

Revisions (0)

No revisions yet.