0
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks, I thought I was wrong when I got different values for i. Your explanation was helpful and cleared my doubts. $\endgroup$ – Jsph Aug 3 '18 at 16:07

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.