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$
1
  • $\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, 2017 at 19:02

1 Answer 1

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.

$\endgroup$
2
  • 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$ Jun 15, 2017 at 15:44
  • 2
    $\begingroup$ @AndrejBauer, story of my life $\endgroup$
    – Covvar
    Aug 14, 2017 at 21:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.