Correctness of programs - Multimedia Introduction to Programming Using Java - page 497

{ perm({x, y}, {X, Y}) } S { perm({x, y}, {X, Y}) and x≤y }
5. Specification of a program S . Print x on the Java console, followed by a line
feed. We can write this as a Hoare triple if we use a String variable javaConsole
(say) to denote the Java console. Again using a virtual constant, we have:

{ javaConsole = JV } S { javaConsole = JV + x + "\n" }
This example shows how we can deal with statements that print on the Java con-
sole or some file.

IV.2 Two inference rules

Suppose we know that the following Hoare triple is true:

{ x≥0 } S { y=x and z = x+1 }
Then, we can also conclude that statement S does its job in an initial state in
which x = 0 and in a final state in which z = x+1:

{ x=0 } S { y=x and z = x+1 }
{ x≥0 } S { z = x+1 }
That is, we can replace the precondition by something that implies it, and we can
replace the postcondition by something that it implies. We might write this as:

{ x = 0 }
{ x ≥ 0 }
S
{ y=x and z = x+1 }
{ z = x+1 }
Thus, if we have two adjacent assertions, the rule is that the first must imply the
second, i.e. whenever the first is true, the second must be true too. We might do
something like this if we are interested only in the “stronger” precondition, in
this case x=0 , or the “weaker” postcondition, in this case, z = x+1 .
To formalize these notions, we use the logical operator implication
operation b => c , which is defined as follows:
Definition of implication =>
false => false is true
false => true is true
true => false is false
true => true is true
Note: Boolean expression P is stronger than boolean expression Q if P is true in
fewer states than Q . We also then say that Q is weaker than P . Here is a more pre-
cise definition: