0
$\begingroup$

I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X}

{X}  
if (b mod 2 <> 0)
      t = 1
else
      t = 0
{t = b – 2*(b div 2)}

Any help would be amazing!

Improve this question
$\endgroup$
2
  • $\begingroup$ The answer depends on the exact semantics of the operations mod and div. You might get away with the empty precondition (which always holds). $\endgroup$
    – Yuval Filmus
    Apr 29, 2021 at 13:46
  • 1
    $\begingroup$ Maybe consider what would make the program crash. Usually preconditions are needed to block that. $\endgroup$
    – ShyPerson
    May 12, 2021 at 20:02

0

Reset to default

Your Answer

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