# Axiomatic Semantics and Postconditions

I'll preface this by saying that this IS a homework question.

However, when asked about how to solve it in class, (I believe) my professor was unable to complete it.

The question is:

Compute the weakest precondition for each of the following assignment statements and postconditions: $$a = a + 2b - 1\ \{a > 1\}$$ (where a > 1 is the postcondition)

His answer was: "$a > 2 - 2b$." Is this correct? It seems that he broke the rules of equivalents, by using the ">" as "="

I believe the answer is: $$\{a>1\;\wedge\; b<\tfrac12\}\quad\text{or}\quad \{a > 0\;\wedge\;2b-1 +a >1\},$$ where the "$\wedge$" symbol means "and"

We're using Concepts of Programming Languages, by Sebesta, 10th Edition, so any references from that material would be excellent :)

Thanks!

• I don't understand your question. Your second suggested answer is equivalent to $\{a>0 \;\wedge\; a>2-2b\}$, which is essentially the same as the answer by your professor that you're rejecting. The difference is that you're also including the requirement $a>0$ for no reason that I can see, so your precondition fails to be a weakest precondition. – David Richerby Feb 6 '14 at 23:05
• instead of telling me how I'm wrong, could you please explain properly? I understand that I am wrong, that is why I asked a question. – FuriousFolder Feb 6 '14 at 23:49

A condition $P$ is weaker than $Q$ if $Q\Rightarrow P$; that is, whenever $Q$ holds, $P$ also holds or, if you prefer, $Q$ guarantees that $P$ holds. $P$ is strictly weaker than $Q$ if $Q\Rightarrow P$ but $P\not\Rightarrow Q$. Let's look at the three conditions included in the question:
1. $a>2-2b$
2. $a>1 \;\wedge\;b>\tfrac12$
3. $a>0 \;\wedge\; a>2-2b$
(2) $\Rightarrow$ (3) since, if $a>1$ then certianly $a>0$ and, if $b>\tfrac12$, then $2-2b<1<a$. (3) $\Rightarrow$ (1) since if $X$ and something else are both true, then certainly $X$ is true. None of the reverse implications holds: (1) is satisfied by $a=-1$, $b=2$ but (3) is not; (3) is satisfied by $a=\tfrac12$, $b=1$ but (2) is not. Therefore, (1) is strictly weaker than (3) which, in turn, is strictly weaker than (2).
So $a>2-2b$ is the weakest of the preconditions on the table. But is it the weakest possible? Suppose $P$ is any precondition that implies that $a+2b-1>1$. Rearranging, we see that $P\Rightarrow a>2-2b$, i.e., $P\Rightarrow$ (1). This tells us that no other precondition can be strictly weaker than (1). Therefore, (1) is the weakest precondition.