I am trying to understand Dijkstra's weakest precondition inference technique using notes from here. I am following a simple example given over there to compute the weakest precondition -
x = x - 2;
z = x + 1;
{ z != 0 }
Here is the solution to this problem -
{ x != -1 }
x = x - 2;
{ x != -1 }
z = x + 1;
{ z != 0 }
I don't understand the part where, { x != -1 }. Shouldn't it be { x != 1 }?
Edit 1
I apologize for not clearly stating my confusion.
I completely understand the precondition { x != -1 } for the statement z = x + 1.
My confusion arises in the following statement - x = x - 2
Over here, we know that we don't want x (rhs) to be -1. Therefore, (if I understand correct) we need to set up a precondition on x (lhs). For {x!=-1}, the lhs x should be {x!=1}.
You are correct. The first precondition should be
{x≠1}, not{x≠-1}. It's probably a typographic error.