How does one identify the weakest preconditions in Hoare triples?

160 Views Asked by At

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}.

1

There are 1 best solutions below

0
On BEST ANSWER

You are correct. The first precondition should be {x≠1}, not {x≠-1}. It's probably a typographic error.