Pre and Post Conditions: Hoare Logic - 2

Continuing the post Hoare Logic - 1, we will now present to which kind of statements these triples (pre, program, post) can be applied
0. Nop (doesn't do anything)
1. Assignments
x := e // x gets the value of some expression e, that may or may not contain x
2. Consequence; that is, S1;S2 (first execute S1, then S2)
3. if B then S1 else S2 fi (typical if, with B a boolean condition)
4. while B do S od (at each iteration, B is checked. If satisfied by the current state, S is executed)

All these statements can then be combined to make more complex programs, and provide the formalization to prove program correctness

For example, given P:

y := 2*x;
if (y < 0) z := - y/2
else z := y/2
fi

we can prove that the value of z is the absolute value of x (the division is the real division, not the integer one).

To do so we can instrument the program above as follows:

1. {\(x=X_0\)}
y := 2*x;
2. {\(x=X_0 \land y = 2\cdot x\)}
if (y < 0)
  z := - y/2
3.  {\(x=X_0 \land y = 2\cdot x \land z = - y/2\)}
else
   z := y/2
4.  {\(x=X_0 \land y = 2\cdot x \land z = y/2\)}
fi

5. {\(x=X_0 \land y = 2\cdot x \land (y<0 \rightarrow z = - y/2)  \land (y\ge 0 \rightarrow z = y/2)\)}

Line 1 adds an auxiliary variable (X₀) - which doesn't appear in the program - to indicate that the contents of x do not change. Auxiliary variables can be added at any stage of the proof, but their value does not change; that is, from the moment we have indicated x = X₀ in 1, we have indicated that X0 will always contain x's initial value

Line 2 adds the assignment to y, and that x has not changed

Line 3 considers the first branch of the if, and Line 4 the second branch, updating z as necessary

Line 5 joins both branches, according to the condition. That is, if y <0 then the first branch is applied, otherwise the second one.

5. {\(x=X_0 \land y = 2\cdot x \land (y<0 \rightarrow z = - y/2)  \land (y\ge 0 \rightarrow z = y/2)\)}
Now given this last expression, we'll try to conclude that indeed z contains the absolute value of x

From
\(x=X_0 \land y = 2\cdot x \land (y<0 \rightarrow z = - y/2)\)
It can be inferred that when y<0 the value of z is -X₀
Similarly, from the second implication it can be inferred that when y is greater or equal than 0, the value of z is X₀.

Now, y is lower than 0 iff x is lower than 0, therefore,
the value of z is -X₀ if x is lower than 0, and X₀ otherwise, which is the definition of the absolute value, as expected.