How to solve for the precondition give a postcondtion that must satisfy two conditions

Question

I tried solving past exam question but there is this one that I haven't been able to solve.

The question states that a suitable precondition should be found for the statement.

$$ a= i +2; i++\{(a = 7)\land(i = 5)\} $$ Here's my solution and where I got stuck:

$$ wp(a= i +2; i++,(a = 7 \land i = 5) \\ =wp(a= i +2, wp(i=i+1,a = 7\land i = 5) $$

I've tried solving it intuitively and I arrive at the conclusion that no such value for ii should exist.

I haven't been able to find a rule to combine the two predicates of the post-condition.

Please I would like to know when solving similar questions can I change the ^ to an algebra symbol or should I take the relevant condition and find the weakest precondition with that.

Answer 1

The rules for $wp$ are straightforward for non-loops:

$$wp(c_1 ; c_2, V) = wp(c_1, wp(c_2, V))$$ $$wp(x := e ; V) = V\left[x \mapsto e\right]$$

Plugging in the original values, you need to compute

$$ wp(a := i + 2; i := i + 1, (a = 7) \wedge (i = 5)) $$

The first rule applies here, giving

$$ wp(a := i + 2, wp(i := i + 1, (a = 7) \wedge (i = 5))) $$

In the second $wp$ expression, the second rule applies, giving

$$ wp(a := i + 2, (a = 7) \wedge (i + 1 = 5)) $$

Now the second rule applies again to the remaining $wp$:

$$ ((i + 2) = 7) \wedge (i + 1 = 5) $$

Now, you just need to know that the above is always false, regardless of the value of $i$. There are various automatic approaches to do this (since these are linear equations, you could use the simplex method). In this case, since they're so simple, you could just normalize your equations into $i = constant$:

$$(i = 7 - 2) \wedge (i = 5 - 1)$$

Knowing $7 - 2$ and $5 -1$ are constant expressions, you can get $$i = 5 \wedge i = 4$$ which would imply $$4 = 5$$ which is always false, so the original statement must be always false.