CS 420: Program Derivation (Spring 2013)

Given a programming problem, how should one go about finding a solution. Is there some discipline that can be followed to arrive at a solution that one can be sure of being correct. As per the 'Correct by Construction' approach to programming, the course will teach how to calculate a program from a given specification of the problem to be solved. That is, how to formally specify a problem and then work backwards from that specification.

Alice: `Would you tell me, please, which way I ought to go from here?'
That depends a good deal on where you want to get to,' said the Cat.

Schedule: Lecture Slot 11 in SIC 301 Kresit
Instructor: Om Damani Office hours: Fri 5-6

Moodle: Slides, Assignments, Solutions, Reference Materals, Newsgroup etc.

Pre-requisites Background in Propositional Logic and Quantifiers
Audit Requirements: You have to pass the course.

Text Books

Unfortunately the following book is out of print. 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-2: 08-11/01 Logistics, Inroduction, Example Problems: specifying max, finding all elements of an array satisfying certain condition logistics
3-5: 15-25/01 Propositional Logic, Quantifier Calculus Ch. 1 and Ch. 3, cached copy of A Programmer's Introduction to Predicate Logic by H. Conrad Cunningham
6: 29/01 Hoare Triple, Weakest Precondition, The Guarded Command Language - Skip, Assignment Ch 2-2.2
7: 01/02 The Guarded Command Language - Catenation Ch 2.3
8: 05/02 The Guarded Command Language - Selection Ch 2.4
9-11: 08-15/02 The Guarded Command Language - Repetition, loop invariant Ch 2.5-2.7
12: 26/02 Program Derivation: Taking a conjunct as guard, 4-tuple sort, integer sq. root, linear search Ch 4.0-4.1, 6.1
13-14: 01-05/03 Replacing constant by variable, divmod, more efficient divmod, exponentiation, Binary Search Ch 4.2, 5.1, 6.3
15: 08/03 Quiz  
16: 12/03 Strengthening invariants, Fibonacci, maxsegsum Ch 4.3
17: 15/03 Tail invariants Ch 4.4
18-19: 19-22/03 Bounded Linear Search, Array Partitioning, more on Tail invariants [kal] Ch 6.2, 10.0 - 10.2.0, 4.4
20: 26/3 Majority Voting
21: 2/4 Tail Recursion - reversing a link list, Post order traversal of a binary tree, -
22-23: 5/4 Searching by Elimination, Making post-condition and prec-condition resemble each-other: Saddleback Search [kal] Ch 8.0-8.1.0 . 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"
24: 9/4 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), TestAllTrue, Using tail-invariant when post-condition is an equation: Decomposition in sum of two squares Dijkstra on tail-invariant, Ch 8.1.1
25: 12/4 All pair shortest path in a graph -