Outline of Class 20

Miscellaneous

• Those of you following the Sun vs. Microsoft Java suit might want to vote in the Ziff-Davis News Poll at http://www.zdnet.com/zdnn/special/sun.html
• Sometime this week, I'll be asking you to take a survey on your use of the course web and on your Meyers-Briggs personality type (this is just a warning so that it won't be a surprise).

Program Correctness

• On Friday, we developed implementations (some correct, some incorrect) of binary search.
• So, how would we be sure that your binary search routine worked?
• We could come up with a set of tests that we expect will stress all the appropriate issues, but we clearly can't test everything. For example, it may be difficult to catch memory leaks if you only test moderate size problems. Nonetheless, testing is a good step on the path to correctness.
• We could attempt to prove the program is correct (in that it meets the specifications). This requires that we understand proof techniques and that we have a method for proving components of a program correct.

Program Proofs

• For algorithms written in procedural languages, we can use program assertions. In effect, before every statement we indicate the expected state of the system, and after every statement we indicate the new state of the system. We can then attempt to show that the statement properly affects the system.
• There are models for the effect of standard statements (e.g., assignment) on the state of the system.
• For loops and related structures, we write loop invariants, conditions we expect to be true before and after each repetition of the loop.
• Depending on what works best, you might do proofs forward or backwards.