CS 420: Program Derivation (Autumn 2011)

Given a [programming] problem to be solved, how should one go about finding a solution [/program]. Is there some discipline that one can follow to arrive at a solution that one can be sure of being correct. In many cases, a solution can be arrived at if one is careful enough about formally specifying what one wants to achieve and then working backwards from that specification. In this context, the course will try to teach how to calculate a program from a given specification of the problem to be solved.

Schedule: Lecture Slot 6 in SIC 301 Kresit
Instructor: Om Damani Office hours: Fri 5-6
TA: Devendra Shelar
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 the following book is not available in Indian edition. The instructor will make the required material available.

1. [Kal] 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.

Lectures

Sr. No: Date Topic Resource
1: 22/07 Logistics, Inroduction, Example Problems: max, finding the common integer in three sorted arrays logistics
2: 27/07 sorting 4 integers, majority voting  
3: 29/07 Propositional Logic, importance of equivalence, all binary operators in terms of equivalence and disjunction Cached copy of A Programmer's Introduction to Predicate Logic by H. Conrad Cunningham
4-5: 3,5/08 Propositional Logic, Predicate Calculus [kal] Ch 1
6-7: 10,12/08 Qunatification Calculus, Specification Examples [kal] Ch 3
8-9: 17,19/08 Guarded Command Language [kal] Ch 2
10-11: 24,26/08 GCL, Deriving loopless programs, Taking a conjunct as invariant [kal] Ch 2, 4.1
12: 02/09 Linear Search [kal] Ch 6.1
13-14: 07-09/09 Multiple solutions to Integer Divison [kal] Ch 4.1
15-16: 21-23/09 More efficient Integer Divison [kal] Ch 5.1
17-18: 28-30/09 Maximum Segment Sum, Inverted Pairs, Binary Search [kal] Ch 4.3. Binary search is given in [kal] 6.3, though we followed Wim Feijen's approach. You can also look at Dijkstra's derivation.
19-20: 5-7/10 Quiz and solution discussion : subsegment having maximal credit [kal] Ex 5 in Ch 4.3
21-22: 12-14/10 Bounded Linear Search, Array Partitioning, Tail Recursion [kal] Ch 6.2, 10.0 - 10.2.0, 4.4
Tutorial: 17/10 Meaning of P(n:=n+1), Program annotation [kal] Ch 4.3
23-24: 19-21/10 Tail Recursion - reversing a link list, Post order traversal of a binary tree, Searching by Elimination, Celebrity problem [kal] Ch 6.4
25-26: 26-28/10 Diwali Holidays  
27: 2/11 Making post-condition and prec-condition resemble each-other: Saddleback Search, Using tail-invariant when post-condition is an equation: Decomposition in sum of two squares [kal] Ch 8.0-8.1.1 . Note that in class we did a non-tail recursive formulation of the saddleback search - the saddleback search discussion in book is based on the concept of "Using tail-invariant when post-condition is an equation"
28: 4/11 No class - Schedule for Tuesday, Reading Assignment: Segment Problems [kal] Ch 7, 8.2
29: 9/11 When tail-invariant is better/needed; when repetition guard is not a conjunct of post-condition but is calculated as a sufficient condition for implying the post-condition (along with invariant) Wim Feijen on tail-invariant and Dijkstra on tail-invariant. Note that in the Wim Feijen's problem, there is no choice but to use a tail-invariant.
30: 11/11 Majority Voting, Specifying Minimum Spanning Tree