Java Reference

In-Depth Information

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
.

Search WWH ::

Custom Search