Java Reference
In-Depth Information
/** =
index of minimum value of
b[h..k]
. Precondition:
h ≤ k. */
public static int
min(
int
[] b,
int
h,
int
k)
Calling this function makes sense only if the array segment has at least one
value; hence the precondition.
How will this function be used?
Examples when
d={1
,
5
,
1
,
7
,
3
,
8}
:
To watch this
algorithm exe-
cute, listen to
activity 8-5.3.
call
result
min(d
,
0
,
5)
0
or
2
min(d
,
1
,
5)
2
min(d
,
3
,
5)
4
min(d
,
1
,
1)
1
The call
min(d
,
0
,
5)
is interesting: the specification does not say which mini-
mum value will be returned if the minimum value occurs more than once.
The heart of this function is a loop to find the index
m
of a minimum value.
We now develop it. Because we are allowed to return the index of
any
smallest
value, we choose to return the first one. Here is the postcondition:
h
m
k
Post
R
:
v
b
>v
≥v
We can get an invariant by replacing
k
by a fresh variable
i
:
h
m
i
k
inv
P
:
v
?
b
>v
≥v
How does it start?
At the beginning, the smallest value found so far is in
b[h]
. So we set both
i
and
m
to
h.
When is it done?
The invariant and postcondition look the same when
i=k
.
How does it make progress?
Increment
i
to make unknown section smaller.
/** =
index of minimum value o
f b[h..k].
Precondition:
h≤k */
public static int
min(
int
[] b,
int
h,
int
k) {
int
m= h;
int
i= h;
// {inv: b[m]
is the minimum of
b[h..i]}
while
(i != k) {
i= i + 1;
if
(b[i] < b[m])
{ m= i; }
}
return
m;
}
Figure 8.6:
Function
min
Search WWH ::
Custom Search