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.
$\begingroup$
$\endgroup$
2
-
3$\begingroup$ Ex falso quodlibet. $\endgroup$– Yuval FilmusJun 14, 2022 at 18:45
-
$\begingroup$ $\text{false}\implies x+1=0$. $\endgroup$– user16034Jun 14, 2022 at 19:18
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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).