Java Reference
In-Depth Information
//
Process the natural numbers
0..s.length()-1
int
k= 0;
// {
invariant:
0..k-1
have been processed
}
while
(k != s.length()) {
Process
k;
k= k + 1;
}
// { 0..s.length()-1
have been processed
}
Next, we replace the abstract specification, postcondition, and invariant by con-
crete ones:
// Set
x
to the number of
w
's in
s[0..s.length()-1]
int
k= 0;
// {
invariant:
x=
number of
w
's in
s[0..k-1] }
while
(k != s.length()) {
Process
k;
k= k + 1;
See lesson
page 7-3 to ob-
tain the loop
}
// { x
= number of
w
's in
s[0..s.length()-1] }
We must initialize so that the invariant is true initially. Since
k
is initially
0
,
to truthify the invariant, set
x
to
0
.
The only thing left to do is to insert code to process character
k
. If this char-
acter is a
w
, then
s
has to be incremented. This leads to the program of Fig. 7.3.
Concluding remarks
This concludes the development of a loop from a loop schema. With this par-
ticular schema, most of the code gets copied over, without change, making the
development easier (and shorter). The main creative parts are to truthify the
invariant initially and to write the implementation of “Process
k
”. To do this cor-
rectly, we first have to write the postcondition and then the invariant.
//
Set
x
to the number of
w
's in
s[0..s.length()-1]
int
k= 0;
x= 0;
// {
invariant:
x
= number of
w
's in
s[0..k-1] }
while
(k != s.length()) {
if
(s.charAt(k) == 'w') {
x= x + 1;
}
k= k + 1;
}
// { x =
number of
w
's in
s[0..s.length()-1] }
Figure 7.3:
Counting the
w
's
Search WWH ::
Custom Search