Java Reference

In-Depth Information

1. {
0 = 0
}
x= 0;
{
x = 0
}

2. {
x+1 = 0
}
x= x+1;
{
x = 0
}

3. {
x + n+1 =
sum of
1..n
}
x= x + n+1;
{
x =
sum of
1..n
}

4. {
x =
sum of
1..n-1
}
n= n-1;
{
x =
sum of
1..n
}

5. {
b = z*x*x
y
}
z= z*x;
{
b = z*x
y
}

6. {
b = z*x*x
y-1
}
y= y-1;
{
b = z*x*x
y
}

7. {
0 = a*(2*y)
2
+ b*(2*y) + c
}
y= 2*y;
{
0 = a*y
2
+ b*y + c
}

Take a look at the following use of the assignment statement axiom:

{
y=0
}
x= e;
{
y=0
}

Any constant could be substituted for
0
, and any variable (except
x
) could be

substituted for
y
. Thus, this Hoare triple indicates that an assignment to
x
cannot

change any other variable! No
side effects
are allowed during evaluation of
e
. For

example, evaluation of
e
cannot call a function that changes a field of an object

that is visible where this assignment statement is, for that would be a side effect.

A form of assignment statement axiom can be developed that caters to side

effects, but it is far more complicated. If you want to use the simple assignment

statement axiom that we have introduced, you cannot allow side effects.

IV.3.3

Multiple assignment statement

A favorite assignment statement among people in the formal development of pro-

grams is the
multiple assignment statement
, which allows several variables to be

assigned simultaneously. The first multiple assignment below swaps the values

of
x
and
y
. The second rotates the values
u
,
v
, and
w
. With the third, if
x
is
4
ini-

tially, upon termination
x
is
5
and
y
is
4
:

x, y= y, x;

u, v, w= v, w, u;

x, y= x+1, x;

The multiple assignment is not a Java statement. When developing program,

use of the multiple assignment along the way helps understanding and helps

reduce errors. Below is the multiple-assignment definition for assignment to two

variables. It extends in the obvious way to more variables.

Multiple-assignment statement axiom
. For all assertions
R,

{
e
is well-defined and
[v,w\e,f]R
}
v, w= e, f;
{
R
}

IV.3.4

Sequencing

We give an inference rule that allows us to conclude:

Search WWH ::

Custom Search