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

IV.3.1 Empty statement

The empty block {} does absolutely nothing, but very fast. In some languages, it
can be written as skip . In others, a semicolon by itself denotes a skip statement.
Thus:

x= x+1; ;
consists of two statements: the first increments x ; the second does nothing.
We can define the skip as follows:
skip axiom . For all assertions R,
{ R } skip { R }
This makes sense. If R is true, and nothing is done, then R is still true.

IV.3.2 Assignment statement

The assignment statement is defined as follows:

Assignment statement axiom . For all assertions R,
{ e is well-defined and [v\e]R } v= e; { R }
At first glance, this definition looks backward; one feels that the postcondition,
not the precondition, should include [v\e]R , since the assignment stores e in v.
However, the definition is correct. It shows how one can compute the necessary
and sufficient precondition such that execution of the assignment terminates with
R true. We will give examples in a moment.
The first part of the precondition, “ e is well-defined”, is present in order to
ensure that evaluating e does not cause an exception. Here are possible expres-
sions e and the accompanying expression “ e is well defined”:

b[i] 0 ≤ i < b.length
x/y y!=0
s.charAt(k) 0 ≤ k < s.length()
One can use different versions of “e is well-defined”, depending on one's
needs. For example, suppose x and y have type int . Here are two possibilities
for “ x+y is well-defined”. Use the first to get a general handle on correctness of
a program, assuming that “God's integers” are being used; use the second when
complete correctness, down to not having arithmetic overflow, is required:

(1) First alternative: true
(2) Second alternative: abs( x+y) ≤ INTEGER.MAX_VALUE
Below, we give examples of uses of the assignment statement axiom. We omit
the term “ e is well-defined” when it is true .