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