Java Reference
In-Depth Information
//
Process elements of
c[h..k-1]
, in order
//
inv:
h≤i≤k
and
c[h..i-1]
has been processed
for
(
int
i= h; i != k; i= i + 1) {
Process
c[i]
}
We could use either
b
or
result
in place of
c
. We choose
b
, so instead of
h
we
have
x
and instead of
k-1
we have
y
(i.e. instead of
k
we have
y+1)
:
//
Process each element of
b[x..y]
, in order
//
inv
: x≤i≤y+1
and
b[x..i-1]
has been processed
for
(
int
i= x; i != y + 1; i= i + 1) {
Process
b[i]
}
Where in
result
do we put element
b[i]
? The first element
b[x]
goes into
result[0]
, so
b[i]
goes into
result[i - x]
:
result[i - x]= b[i];
The invariant must say that everything before index
i
has been copied:
inv:
b[x..i-1]
has been copied to
result[0..i-x-1]
After the loop terminates, the array segment has been copied to
result
.
This completes the development of the function to copy an array segment.
See Fig. 8.4 for the function.
8.4
Storing tables of values in arrays
Consider maintaining a table of results of experiments, perhaps the number of
seconds it takes a rat to run through a maze. A program may start off with no
results in an array
runningTimes
(say) and, as the rat is run through the maze
again and again, new results are added. Since the array size is given when the
array is first created, the size must be large enough to contain all the experiment
/** =
a copy of array segment
b[x..y] */
public static int
[] copy(
int
[] b,
int
x,
int
y) {
int
[] result=
new int
[x+1-y];
//
Process each element of
b[x..y]
, in order
// inv: x ≤ i ≤ y + 1 and b[x..i-1]
has been copied to
c[0..i-x-
1
]
for
(
int
i= x; i != y+1; i= i + 1) {
result[i - x]= b[i];
}
return
result;
}
Figure 8.4:
A function to copy an array segment
Search WWH ::
Custom Search