CS 420: Program Derivation (Fall 2014)

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 6 in SIC 201 Kresit
Instructor: Om Damani

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

Pre-requisites Background in Propositional Logic and Quantifiers
Audit Requirements: You have to do all assignments.

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: 23-30/07	Background quiz, Logistics, Inroduction, Example Problems: specifying and derving max	logistics
3-5: 1,6,8/08	Formal Specifications, Quantified Operators	Ch. 1 and Ch. 3, cached copy of A Programmer's Introduction to Predicate Logic by H. Conrad Cunningham
6: 13/08	Hoare Triple, Weakest Precondition, The Guarded Command Language - Skip, Assignment, Catenation	Ch 2-2.3
7: 14/08	The Guarded Command Language - Selection	Ch 2.4
8-9: 20,22/08	The Guarded Command Language - Repetition, loop invariant, exponentiation	Ch 2.5-2.7, Only exponentiation proof (not derivation) part of 4.2 and 4.4
10: 27/08	Deriving loopless programs, taking conjunct as invariant, linear search	Ch 4.1, 6.1
11: 03/09	basic divmod, making it efficient	Ch 4.1, 5.1
12-13: 17-19/09	Midsem soln., Concept of Fully annotated program, Replacing constants by variables, Strengthening Invariants	Ch 4.2, 4.3
14-15: 24-26/09	Strengthening Invariants, Tain Invariants	Ch 4.3, 4.4
16-26:	Applying above techniques in various situations, CAPS tool	Ch 7,8,12