World's most popular travel blog for travel bloggers.

# [Solved]: Axiomatic Semantics and Postconditions

, ,
Problem Detail:

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!

#### Answered By : David Richerby

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.