Permalink
Cannot retrieve contributors at this time
PhDThesis/incomingTheory.tex
Go to fileProduct: | |
an assessment instrument/list of questions for incoming to algorithms, | |
in which we expect to see proofs about resource utilization | |
Recall proof by mathematic induction:\\ | |
There is a proposition, $p$, that we want to show to be true for some domain (i.e., set) $D$. | |
There is some correspondence between the elements of $D$ and the natural numbers. | |
When the corresponding natural number, k, is at some value, say $k_0$ for which we can readily show that p is true, we take advantage of that ease, and prove $p(k_0)$, that is to say, prove the proposition p is true for the case $k_0$.\\ | |
Next we need to have a link, from one case to another. Consider a sequence, i.e., the idea "next" makes sense. Then, the implication "$p$ is true of k implies that $p$ is true of next(k) provides a link. We have a successor function for the natural numbers; the next natural number is obtained by adding 1. Consider the implication "$p$ is true of k implies that $p$ is true of $k+1$. | |
We can combine a base case, $p(k_0)$ with a linking implication, $p(k) \implies p(k+1)$, where the context in which the linking implication is true includes $k_0$, to show that $p$ is true of all the elements of the domain that are greater than or equal to $k_0$. | |
The above considerations make useful the following two part procedure. | |
Find a base case and prove it. | |
Find a linking implication and prove it, for a domain including the base case. | |
\begin{enumerate} | |
\item Proofs of Termination | |
\begin{enumerate} | |
\item for ($i=0;i<10;i++$)\{\\ | |
disp(i);\\ | |
\}\\ | |
Assuming there is no problem with disp, how do we prove that this loop terminates? | |
\item for ($i=0;i>10;i--$)\{\\ | |
disp(i);\\ | |
\}\\ | |
Assuming there is no problem with disp, how do we prove that this loop terminates? | |
\item for ($i=n;i>0;i--$)\{\\ | |
disp(i);\\ | |
\}\\ | |
Assuming there is no problem with disp, how do we prove that this loop terminates? | |
\item | |
i=n; | |
while ($i>n$)\{\\ | |
disp(i);\\ | |
i--; | |
\}\\ | |
Assuming there is no problem with disp, how do we prove that this loop terminates? | |
\item | |
i=n; | |
while ($<some\;\;condition>$)\{\\ | |
disp(i);\\ | |
update(condition); | |
\}\\ | |
Assuming there is no problem with disp or update, how do we prove that this loop terminates? | |
\end{enumerate} | |
\item Proofs by Loop Invariant \\ | |
Consider the following situation:\\ | |
There is a proposition, $p$, that we want to show to be true for some domain (i.e., set) $D$, \textbf{and we will process elements of that domain using a loop}. | |
There is some correspondence between the elements of $D$ and the natural numbers. | |
When the corresponding natural number, k, is at some value, say $k_0$ for which we can readily show that p is true, we take advantage of that ease, and prove $p(k_0)$, that is to say, prove the proposition p is true for the case $k_0$. \textbf{We will choose our loop variable's first value to be $k_0$.}\\ | |
Next we need to have a link, from one case to another. Consider a sequence, i.e., the idea "next" makes sense. Then, the implication "$p$ is true of k implies that $p$ is true of next(k) provides a link. We have a successor function for the natural numbers; the next natural number is obtained by adding 1. Consider the implication "$p$ is true of k implies that $p$ is true of \textbf{next($k$). The loop specification produces a sequence, defining "next".} | |
We can combine a base case, $p(k_0)$ with a linking implication, $p(k) \implies p($next($k)$, where the context in which the linking implication is true includes $k_0$, to show that $p$ is true of all the elements of the domain that are \textbf{next after} or equal to $k_0$. | |
The above considerations make useful the following two part procedure. | |
Find a base case and prove it. | |
Find a linking implication and prove it, for a domain including the base case. | |
In the specific situation of proof by loop invariant, these procedure steps are called:\\ | |
Prove that the property is true before the loop starts. | |
Prove that what happens in the loop does not, at the end of any single loop iteration, change the property to false. | |
\item | |
\end{enumerate} | |