blob: 4afd1e388ab8248913a8d692bf881b703353c670 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
HI10: This example gives examples of heavily and lightly documented pieces
of code.
@O@<hi10.out@>==@{
@<Set p to the length of the longest plateau in sorted array b[1..N]@>
@<Function comp@>
@}
@A@<Calculation of the longest plateau in array b@>
This section contains a solution to a problem outlined in section 16.3 of
the book @/The Science of Programming@/ by David Gries[Gries81].
@B Given a sorted array @{b[1..N]@} of integers, we wish to determine the
@/length@/ of the longest run of identically valued elements in the array.
This problem is defined by the following precondition and postcondition.
@$@<Precondition@>==@{/* Pre: sorted(b). */@}
@$@<Postcondition@>==@{@-
/* Post: sorted(b) and p is the length of the longest run in b[1..N]. */@}
@B We approach a solution to the problem by deciding to try the approach of
scanning through the array one element at a time maintaining a useful
invariant through each iteration. A loop variable
array index @{i@} is created for this purpose. The bound function is
@{N-i@}. Here is the invariant.
@$@<Invariant@>==@{@-
/* Invariant: sorted(b) and 1<=i<=N and */
/* p is len of longest run in b[1..i]. */@}
@B Establishing the invariant above in the initial, degenerate case is easy.
@$@<Establish the plateau loop invariant initially@>==@{i=1; p=1;@}
@B At this stage, we have the following loop structure. Note that when both
the invariant and @{i != N@} are true, the postcondition holds and the loop
can terminate.
@$@<Set p to the length of the longest plateau in sorted array b[1..N]@>==@{@-
@<Precondition@>
@<Establish the plateau loop invariant initially@>
while (i != N)
{
@<Invariant@>
@<Loop body@>
}
@<Postcondition@>
@}
@B Now there remains only the loop body whose sole task is to increase @{i@}
(and so decrease the value of the bound function) while maintaining the
invariant. If @{p@} is the length of the longest run
seen so far (i.e. in b[1..i]), then, because the array is sorted,
the extension of our array range to
@{b[1..i+1]@} can only result in an increase in @{p@} if the new element
terminates a run of length @{p+1@}. The increase can be at most 1. Because
the array is sorted, we need
only compare the endpoints of this possible run to see if it exists. This
is performed as shown below.
@$@<Loop body@>==@{i++; if (b[i] != b[i-p]) p++;@}
@A The following function compares two C~strings and returns TRUE iff they
are identical.
@$@<Function comp@>==@{@-
bool comp(p,q)
char *p,*q;
{
while (TRUE)
{
if (*p != *q ) return FALSE;
if (*p == '\0') return TRUE;
p++; q++;
}
}
@}
|
