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!

$\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$ Commented 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
    Commented May 12, 2021 at 20:02

0

Your Answer

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