2.1
In this section:
2.1-2
Predicate: the variable sum
contains the algebraic sum of all elements of A[1:i - 1]
at the beginning of each iteration of the for
loop.
- Initialisation — we initially have
A[0]
,sum = 0
, outside of the array, for a sub-array of 0 elements. Thesum
thus is 0. - Maintenance — assume the invariant holds true for some iteration . Then, for . Before the loop, we have the sum of all elements from . We add
A[k + 1]
to sum, effectively summing everything. - Termination — our loop terminates after we finish
A[n]
, i.e., .
2.1-4
Predicate: the sub-array A[0:i - 1]
does not have the search element s
at the beginning of an iteration i
of the for
loop OR i
holds the first occurrence of s
in A
.
- Initialisation — we initially have an empty array, so .
- Maintenance — assume the invariant holds true for some iteration . Then, for . Before the loop, we have a sub-array
A[0:k]
that doesn’t contains
.- We have two cases: one where it is and one where it isn’t. If it isn’t, then the predicate still holds true for the next iteration.
- If it is, the loop immediately terminates and the second statement is true.
- Termination — the loop either terminates if or if the search element is found.
2.3
2.3-4
For the base case, . Then, . So we’re good for now.
For the case where , where and is an exact power of 2, we have:
We assume this holds true. Then, for , we have: