Question

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!

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top