0
$\begingroup$

My lecturer recently released solutions to an assignment. One of the questions was to determine the weakest precondition of:

{y < 10} if (x > 0 OR y < 10) -> y:=10 fi {true}

According to the provided solution, the weakest precondition of the selection command

(x > 0 OR y < 10) -> y:=10

is

(x > 0 OR y < 10)

I understand how the weakest predicate was arrived at, but why does the solution then state that the total assertion is true because

 (y < 10) IMPLIES EVERYWHERE (x > 0 OR y < 10)

Isn't y < 10 weaker than (x > 0 OR y < 10)? Therefore, there are potential precondition states where y < 10 but x !> 0. Since the program doesn't have guards for such a condition, it then aborts.

$\endgroup$
  • $\begingroup$ " v " stands for or, the upside down " v " stands for and. So your title is wrong, inside the question it's correct. $\endgroup$ – gnasher729 Aug 14 '17 at 19:02
1
$\begingroup$

I'm an idiot.

Of course (y < 10) implies (x > 0 OR y < 10). I was somehow mistaking OR for AND. I'm dumb.

| cite | improve this answer | |
$\endgroup$
  • 9
    $\begingroup$ You're not dumb, you just need to learn to sit on your hands for 5 minutes before you post to stackexchange. $\endgroup$ – Andrej Bauer Jun 15 '17 at 15:44
  • 2
    $\begingroup$ @AndrejBauer, story of my life $\endgroup$ – Covvar Aug 14 '17 at 21:36

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.