2
$\begingroup$

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!

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – David Richerby Feb 6 '14 at 23:05
  • $\begingroup$ 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. $\endgroup$ – FuriousFolder Feb 6 '14 at 23:49
2
$\begingroup$

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.

I don't understand what you mean by `It seems that he broke the rules of equivalents, by using the ">" as "="' since, surely, if (1) breaks that rule, (3) does too? I don't know that rule so maybe somebody else can address that part of the question.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.