Course objectives
The main goal of Com S 400 is to give students a skill in the development of algorithms, based on a practical theory of program correctness. The formal theory is not always used in a formal manner, but it influences the programmer to think in terms of developing a program and its proof of correctness hand-in-hand, with the proof ideas leading the way. The student will learn that use of the program methodology can lead to simpler and more efficient algorithms

Topics covered

• Propositional and predicate calculus. We provide a useful logic, unlike the ones that logicians propose. It is based on substitution of equals for equals, a principle given to us by Leibniz about 400 years ago. It is the basis for proofs in many areas of mathematics. With this logical calculus, we can explain real principles and strategies for the development of proofs. This calculus will be used in a practical way while developing algorithms.
• Weakest preconditions. We study an axiomatic definition of a small programming language, Dijkstra's "guarded commands". This little language, which includes a multiple assignment statement, a nondeterministic conditional statement, and a nondeterminiatic loop, will be used when developing algorithms. The axiomatic definition is in terms of the correctness of algorithms, not in terms of how they are execeuted.
• Formal development of algorithms. We study a methodology for the development of algorithms, which is based on the theory of correctness (weakest preconditions). This major part of the course will introduce and use principles and strategies to be used in algorithmic developments. At the beginning, we will look at basic algorithms that the instructor has developed in the past. But we can look at new problems as well. Where we go in this endeavor will depend on the class participants.
• Problem solving. Many of the principles, strategies, and ideas used in developing proofs in our logical calculus and in the formal development of algorithms can be used in solving other kinds of problems as well. We will explore some of these problems.

Course outcomes. The student will:

1. Have a skill in the logical calculus and in the formal development of algorithms.
2. Use this skill in an informal way when developing algorithms/programs.
3. Have an appreciation for simplicity and beauty of well-crafted algorithms. CS already has its "computational complexity"; we rely on computational simplicity.