| home page - news - syllabus - topics - schedule - assignments - tutorials - tests - java - references - Mike Jacobson |
| Introduction - Correctness of Algorithms - Analysis of Algorithms - ADTs, Stacks, Queues - Dictionaries - Searching and Sorting - Graph Algorithms |
| Correctness of Algorithms |
In this course we are considering problems that are relatively simple and well-understood. It is therefore reasonable to expect that they can be completely solved using computer programs. The information that follows concerns such problems and the algorithms and programs one would consider for them.
The kind of computational problem that will be considered in this course can generally be described by the following:
Precondition: A description of the problem’s inputs, including their types as well as any relationships or properties that they must satisfy.
Postcondition: A description of the problem’s outputs, including all relationships and properties — involving both inputs and inputs — that must be satisfied when the problem has been “solved.”
A proof of correctness of an algorithm is a mathematical proof of the following: Whenever the algorithm is run on a set of inputs that satisfy a problem’s precondition, the algorithm halts, and its outputs (and inputs) satisfy the problem’s postcondition.
A proof that a program is correct often has two pieces (that can be developed separately):
Proof of partial correctness: This is a proof that, whenever an algorithm is run on a set of inputs satisfying the problem’s precondition, either
So, an algorithm might be “partially correct” because it never, ever halts.
Proof of termination: This is a proof that the algorithm always halts, whenever it is run on a set of inputs that satisfy the precondition.
Various strategies have been found to prove the correctness of different kinds of algorithms — including single statements, sequences of simpler programs, tests, and loops. As time permits, some of these strategies will be described.
The slides used to present this material in class and an exercise on this topic are now available online.
Unfortunately, there are virtually no (nontrivial) computer programs that actually are correct immediately after they have been written: At the very least syntax and similar minor programming errors tend to get made.
The main idea of “software testing” is to show that a program is incorrect, by exhibiting one or more sets of program inputs that cause the program to behave in an unexpected way. One can then try to debug the program in order to find and remove the error (or errors) that caused the program to misbehave.
Additional information about testing and debugging will be provided in class. As time permits, this will either include information about the following, or references for further reading.
The slides used to present this material in class and an exercise on this topic are now available online.
Section 4.5 of the current edition of Discrete Mathematics with Applications discusses proofs of the correctness of algorithms as an application of mathematical induction. The presentation in this text is somewhat nonstandard, because “partial correctness” and “termination” are not considered separately. However, this appears to be a very good introduction to this topic in other respects.
Chapter 2 of the course textbook introduces a “loop invariant” and uses this to prove the partial correctness of a sorting algorithm. On the other hand, proving termination is not really considered as a separate (and distinct) topic. Instead the fact that the algorithm always terminates is a consequence of the fact that it terminates quickly. Thus it is part of the material in the textbook that we will consider next.
The online encyclopedia Wikipedia currently includes a variety of useful articles about software development. It has both a short article on correctness of algorithms and a longer article on Hoare logic, which includes a more formal and detailed presentation of the ideas that are mentioned in lectures.
The online encyclopedia Wikipedia includes an extensive set of articles on testing. Most are reachable from the main article on software testing. This encyclopia includes useful information about debugging as well.
It is unlikely that students will be asked to write complete and formal proofs of the correctness of any algorithms, in this course. On the other hand, you should be prepared to do this in computer science courses that you take later on!
You will be expected to be able to read and understand such proofs in this course: The textbook includes sketches of proofs of some of the algorithms that will be discussed, and the instructor will be sketching proofs of correctness of algorithms in class as well.
You will also be expected to write suitable assertions of various types, including preconditions, postconditions, and loop invariants. You will be asked to included these for all functions and loops in your assignments, and may be asked to write them on tests and the exam.
Similarly, it is not likely that students will be asked to develop extensive suites of tests for programs, carry such tests out, or describe the process they use to debug programs after errors are found.
However, students certainly will be asked to write programs to solve problems on assignments and, of course, the marks received for these programs will be considerably higher if the programs are correct! Consequently, you will likely receive a better mark in this course, than you otherwise would, if you take the time to learn more about test design and implementation, and debugging, and if you apply this to the programs that you submit for assignments in this course. You will be asked to submit documentation describing your testing procedure on all assignments.
What are a precondition and a poscondition? How do these define a computational problem?
What does it mean for an algorithm — that is supposed to solve a given computational problem — to be (functionally) correct?
What are “partial correctness” and “termination”? How are these concepts related to the concept of (functional) correctness?
In what way can you use “divide and conquer” to prove that a long program does what it is supposed to?
What is a “loop invariant”? How do you use this to prove that a while-loop does what it is supposed to?
What should you do (or try to find) in order to prove that a while-loop terminates?
What is the goal of “testing”?
Can you use testing to show that a program is correct? Why (or why not)?
What is unit testing? Name and describe some strategies that can be used to design unit tests.
What are white-box testing and black-box testing?
What is system testing?
What kinds of additional software do you generally need to write in order to carry out tests, once a set of tests has been designed?
What should you do in order to make it more likely that software debugging is successful (that is, removes bugs instead or replacing them or, even worse, increasing them)?
It is useful to know about both proofs of correctness and software testing. Why?
Developers rarely have time to write complete and formal proofs of the correctness of the programs they write. Why might it be useful to know about “proofs of correctness” in spite of this?
The efficiency of algorithms will be considered after this.
|
This page last modified:
http://www.cpsc.ucalgary.ca/~jacobs/cpsc331/W07/topics/correctness.html |