How can i derive this Hoare Tripel?

{false} x := x + 1; {x = 0}

I do not know which rule should i use on this. I am confused on this wrong precondition.

  • 3
    $\begingroup$ Ex falso quodlibet. $\endgroup$ Jun 14, 2022 at 18:45
  • $\begingroup$ $\text{false}\implies x+1=0$. $\endgroup$
    – user16034
    Jun 14, 2022 at 19:18

1 Answer 1


Hoare triple derivations use axioms and rules of Hoare logic. In this case, one would use (1) an instance of the assigment axiom followed by (2) an instance of the consequence rule. Yves Daoust's comment spells out the relevant premise (2).


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.

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