1
$\begingroup$

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

$\endgroup$
0

1 Answer 1

Reset to default
1
$\begingroup$

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .