Array Sum#
Contents#
INPUT an array A[0:n - 1] of n values where n >= 0
OUTPUT an integer sum of the values in A
SUM_ARRAY(A, n)
1 sum = 0
2 for i = 0 to n - 1
3 sum = sum + A[i]
4 return sum
ALTERNATIVELY
SUM_ARRAY(A, n)
1 sum = 0, i = 0
2 while i < n
3 sum = sum + A[i]
4 return sum
\(\textbf{Precondition}\)
\(A\) is a zero-indexed array of \(n\) integers where \(n \ge 0\).
\(i = 0\)
\(\texttt{sum} = 0\)
\(\textbf{Condition}\)
\(i \lt n\)
\(\textbf{Invariant}\)
1. \(0 \le i \le n\)
2. \(\texttt{sum}\) contains the sum of the first \(i\) integers of \(A\): \(\texttt{sum} = \sum_{k = 0}^{i - 1} A[k]\)
\(\textbf{Variant}\)
\(n - i\)
\(\textbf{Postcondition}\)
\(\texttt{sum} = \sum_{k = 0}^{n - 1} A[k]\)
\(\textbf{Initialization}\)
1. \(0 \le \underset{i}{0} \le \underset{n}{\text{nonnegative integer}}\)
\(0 = \texttt{sum} = \sum_{k = 0}^{i - 1} A[k]\)
\(\textbf{Maintenance}\)
Suppose the invariant is true after \(k\) iterations.
1. \(0 \le i \le n\)
2. \(\texttt{sum}\) contains the sum of the first \(k\) integers of \(A\): \(\texttt{sum} = \sum_{k = 0}^{i - 1} A[k]\)
It must be shown that the invariant is true after \(k + 1\) iterations.
1. \(0 \le i' \le n\)
2. \(\texttt{sum}'\) contains the sum of the first \(k + 1\) integers of \(A\): \(\texttt{sum}' = \sum_{k = 0}^{i' - 1} A[k]\)
The condition \(i \lt n\) holds. Therefore \(i + 1 = i' \le n\) and so the first clause of the invariant holds.
\(\texttt{sum}' = \sum_{k = 0}^{i} A[k] = \sum_{k = 0}^{i - 1} A[k] + A[i] = \texttt{sum} + A[i]\)
\(\textbf{Termination}\)
Implementations#
C#
int sum (int A[], int n) {
int sum = 0;
for (int i = 0; i < n; i++) {
sum += A[i];
}
return sum;
}