Unit 2.2 An outline for reasoning about a loop
Link to Logic 2.1.
The mathematical notation that makes the "dot-dot-dot" in
\begin{equation*}
a_0 + a_1 x + a_2 x^2 + \cdots + a_{n-1} x^{n-1}
\end{equation*}
precise is the quantifier \(\sum \text{:}\)
\begin{equation*}
\sum_{i=0}^{n-1} a_i x^i = a_0 + a_1 x + a_2 x^2 + \cdots + a_{n-1} x^{n-1}
\end{equation*}
Importantly, the summation over the empty range equals zero:
\begin{equation*}
\sum_{i=0}^{-1} a_i x^i = 0.
\end{equation*}
Consider evaluating
\begin{equation*}
y :=
% a_0 + a_1 x + a_2 x^2 + \cdots + a_{n-1} x^{n-1} =
\sum_{i=0}^{n-1} a_i x^i ,
\end{equation*}
where \(n \ge 0 \) is an integer. How do we show that
\begin{equation*}
\begin{array}[t]{l}
{\bf Algorithm~1:} \\
y := 0 \\
k := 0 \\
{\bf while~} k \neq n \\
~~~ y := y + a_{k} \times x^k \\
~~~ k := k + 1 \\
{\bf endwhile}
\end{array}
\end{equation*}
computes \(y \text{?}\)
Link to Logic 2.2.
In mathematical logic, a predicate is an expression that evaluates to true or false depending on the values of variables encountered in that expression.
To reason about the algorithm, we add assertions about what must be true at the various points (indicated by the gray boxes and enclosed by curly brackets) in the algorithm:
