CS 420: Program Derivation (Spring 2010)

Schedule: Lecture: Slot 2 in SIC 301 Kresit
Instructor: Om Damani Office hours: M,Thu 5-6
TAs: Dipak Chaudhari and Pratik Jawanpuria
Moodle: Slides, Assignments, Solution, Newsgroup etc.

Pre-requisites Background in Propositional Logic and Quantifiers
Audit Requirements: You have to do all the assignments. There will be at least one assignment per week.

Text Books

Unfortunately these books are not available in Indian editions. The instructor will make the required material available.

1. [Cohen] Edward Cohen, Programming in the 1990s - An introduction to the Calculation of Programs, Springer-Verlag, 1990.
2. [Kaldewaij] Anne Kaldewaij, Programming: The Derivation of Algorithms, Prentice Hall International, 1990.

Reference Books

1. [Dij] Edsger W. Dijkstra, A Method of Programming, Addidon-Wesley, 1988.
2. [DijSch] Edsger W. Dijkstra and Carel S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, 1990.

Lectures

Sr. No: Date Topic Resource
1: 05/01 Logistics, Max of two integers Logistics
2/3: 07,11/01 'Corporate Crook' problem: Finding a common entry in three sorted lists Ascending functions and The Welfare Crook
4: 12/01 Partitioning Problem (related to Quicksort) Pages 12-15 of Sequencing Primitives Revisited for Dijkstra's Dutch National Flag Problem that introduced the 3-way, in-place partition.
5: 14/01 Cake Cutting Problem [Cohen] Ch 0
6,7: 18,19/01 Propositional Logic, importance of equivalence, all binary operators in terms of equivalence and disjunction [DijSch] Ch 1,2,5; [Cohen] Ch 2; Cached copy of A Programmer's Introduction to Predicate Logic by H. Conrad Cunningham
8,9,10: 21,25,27/01 Quantifiers of logical and arithmetic operators [Cohen] Ch 3; Cunningham
11,12: 28/01,01/02 Practice with quantifiers of logical and arithmetic operators [Cohen] Ch 3; [Kaldewaij] Ch 3
13: 02/02 Program Specification: Hoare Triple [Cohen] Ch 4
14: 08/02 Meaning of a Program to satisfy its Specification: Weakest Precondition [Kaldewaij] Ch 2
15,16: 09/02,11/02 The Guarded Command Language [Cohen] Ch 5.4; [Kaldewaij] Ch 2
17: 22/02 Loop Termination; Program Development - sorting 4 integers [Cohen] Ch 5.4.4; [Kaldewaij] Ch 2
18: 23/02 Program Development examples: computing sqrt, linear search [Cohen] Ch 8,9; [Kaldewaij] Ch 4.0-4.2, 6.1
19: 24/02 Midsem Answers
20: 25/02 Computing Integer Division [Cohen] Ch 9.4; [Kaldewaij] Ch 5.1
21: 02/03 Finding the minimum value in an array [Cohen] Ch 10.2
22: 03/03 Evaluating a Polynomial [Kaldewaij] Ch 4.2 Ex 4.2.4
23: 04/03 Finding the location of the minimum element From [Dij], but our own derivation
24: 10/03 The Maximum Section Sum [Cohen] Ch. 10.5
25: 15/03 The Bounded Linear Search [Cohen] 10.8; A derivation of linear search and bounded linear search
26: 17/03 The Binary Search [Cohen] 10.6, though we followed Wim Feijen's approach. You can also look at Dijkstra's derivation.
27: 18/03 Array Rearrangement [Cohen] 10.7. We followed [Kal] 10.2.0 to begin with and discussed various possible derivations. Also check pages 12-15 of Sequencing Primitives Revisited for Dijkstra's introduction of the Dutch National Flag Problem.
28: 22/03 Iterative programs for computing Tail-Recursive functions; Ex: the sum of digits, finding maximum [Cohen] 11.0-11.2, [Kal] 4.
29: 23/03 Tail recursion as means to finding loop-invariants [Kal] 4.4
30: 24/03 Tutorial: discussion of the assignment on - The maximal AB segment
31: 25/03 Exponentiation [Cohen] 11.3
32: 29/03 Sequences, Reversing a Sequence [Cohen] 11.4-5
33: 30/03 Binary Tree, Post-Order Traversal [Cohen] 11.6
34: 31/03 Tutorial
35: 01/04 Depth of a Binary Tree, Fusc [Cohen] 11.7
36: 05/04 Finding max, Searching by elimination, celebrity problem [Kal] 6.4
37: 06/04 Saddleback Search [Kal] 8.1
38: 08/04 Saddleback Search continued, Decomposition in a sum of two squares [Kal] 8.1
39: 12/04 Smallest Segment whose sum is above a given number [Kal] 8.2.2, Ex. 8.2.0
40: 13/04 Majority Voting The Boyer-Moore Majority Vote Algorithm by Wim H. Hesselink
41: 15/04 Some Mathematical Problems