# Finding weakest precondition

I have the following program

x := y + 1;
if (y > 0) then
x := x + y
else x := y + 100;
x := x + y;


I want to compute the weakest precondition for getting {x = y} by executing this program.

The solution of this problem is the following

{(y > 0 & y + 1 + y = 0) | (y = -100)} = {( y > 0 & y = -0.5 | y = -100} = {false | y = -100}
x := y + 1;
{(y > 0 & x + y = 0) | (y =< 0 & y=-100)} = {(y > 0 & x + y = 0) | (y = -100)}
if (y > 0) then
{x + y = 0}
x := x + y
{x=0}
{y + 200 = 0} = {y = -100}
else x := y + 100;
{x=0}
{x+y = y} = {x=0}
x := x + y;
{x=y}


Can anyone explain this solution with a breakdown for each line?

Weakest precondition (WPC) can be computed with a procedure that takes your program, as well as the given postcondition (in this case, x=y), as inputs, and applies certain rules on how the precondition is computed for each part of the program (e.g. how to compute WPC for an if statement), until it reaches the point of computing the precondition for the whole program. Now, since the program you've given is a sequence of statements, this procedure will compute WPC for each of these statements and effectively start with computing WPC for the last statement and "propagate" WPC back to the first statement in the sequence.

In order to understand computation of WPC, it's good to be aware of some relevant notions like the semantics of the programming language your program is given in, i.e. what each statement means, (for your example the semantics is quite straitghforward), the way the WPC is computed according to rules that depend on the given part of the program and its semantics, and then specific rules on how WPC is computed for the given language. (Some links to useful materials are given at the end.)

Specifically for your program, which we will label for more convenient notation of P[x..y], which designates the program part consisting of lines from x to y

1. x := y + 1;
2. if (y > 0) then
3. x := x + y
4. else x := y + 100;
5. x := x + y;


the procedure for computing WPC would be given as

wpc(P, x==y) === wpc(P[1..5], x==y) === wpc(P[1], wpc(P[2..5], x==y))


where we use === for equivalence on the top-level (not be confused with assignments = and equality == in the language), and in turn

wpc(P[2..5], x==y) === wpc(P[2..4], wpc(P[5], x==y))


as P[2..4] represents the if statement. Now,

wpc(P[5], x==y) === wpc(x := x + y, x==y) === x + y == y === x = 0


given the rule for handling assignments, wp(x:=E,R) = R[x ← E], which says that, intuitively, in order for some condition to hold after the assignment of x is executed, same condition should hold before that assignment, where instead of x we have the right-hand side of the assignment, since that will exactly be the value of x after assignment is done.

The next step is computing wpc(P[2..4], wpc(P[5], x==y)), i.e. wpc(P[2..4], x=0), since based on the WPC computation we discussed above, wpc(P[5], x==y) === x==0.

Now, there is again one statement (the if-condition) and one postcondition. (Note that you've written this postcondition two times, once for each branch of the if statement). Without going into all the details, the WPC computation would follow the rule for conditionals, i.e. wp(𝐢𝐟 E 𝐭𝐡𝐞𝐧 S_1 𝐞𝐥𝐬𝐞 S_2 𝐞𝐧𝐝,R) = (E ∧ wp(S_1,R)) ∨ (¬E ∧ wp(S_2,R)), which guarantees the postcondition is satisfied if either branch is taken, thus the WPC becomes a logical OR between WPCs for each branch computed separately, i.e.

wpc(P[2..4], x==0) === (y > 0) & wpc(x := x + y, x==0) | !(y>0) & wpc(x := y + 100, x==0)


which is the same as the condition you wrote

(y > 0 & x + y = 0) | (y =< 0 & y=-100) === (y > 0 & x + y = 0) | (y = -100)


where WPCs for both branches are computed similarly as given before, as both of them represent assignments.

There are many good resources that cover program semantics and generation of verification conditions (including the computation of weakest precondition): some of them are mentioned on Wikipedia, while some courses like the "Program Analysis" course provide good views on the material and might represent a good step to start.