1st Semester 2011/12: Purely Functional Algorithm Specification

Instructors

Jan van Eijck
If you are interested in this project, please contact Jan by email.

ECTS

6

Description

This project explores a new perspective on algorithm specification, in terms of purely functional programming. An algorithm is an effective method expressed as a list of instructions describing a computation for calculating a result. Algorithms have to be written in human readable form, either using pseudocode (natural language looking like executable code), a high level specification language like Dijkstra's Guarded Command Language, or an executable formal specification formalism like Z.

The project will develop an easy purely functional implementation of the Guarded Command Language, and demonstrate how this can be used for specifying (executable) algorithms, and for automated testing of Hoare correctness statements about these algorithms. The small extension of Haskell that we will present and discuss can be viewed as a domain specific language for algorithm specification and testing. Inspiration for this was the talk by Leslie Lamport at CWI on the executable algorithm specification language PlusCal [5], plus Edsger W. Dijkstra, "EWD472: Guarded commands, non-determinacy and formal derivation of programs." [2]. Instead of formal program derivation, we demonstrate test automation of Hoare style assertions.

The project will start with a lightning introduction to functional programming [3]. Next we will review the implementation of the Guarded Command Language in Haskell [2], and the perspective on correctness reasoning about algorithms from [4], and turn to algorithm specification. The final deliverable of the project will consist of a number of algorithm specifications [6] in our domain specific language, written in literate programming style, together with testing code using the QuickCheck tool [1].

The project will be used to develop material for the ESSLLI 2012 course on the same topic that I am preparing right now. See http://homepages.cwi.nl/~jve/pfas for further details.

Prerequisites

Some familiarity with (functional) programming. Interest in algorithm specification.

References

1. K. Claessen and J. Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proc. International Conference on Functional Programming (ICFP), ACM SIGPLAN, 2000.
2. E.W. Dijkstra. Guarded commands, nondeterminacy and the formal derivation of programs. Communications of the ACM, 18:453-457, 1975.
3. K. Doets and J. van Eijck. The Haskell Road to Logic, Maths and Programming. Volume 4 of Texts in Computing. College Publications, London, 2004.
4. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):567-580, 583, 1969.
5. L. Lamport. The PlusCal algorithm language. In M. Leucker and C. Morgan, editors, Theoretical Aspects of Computing - ICTAC 2009, number 5684 in Lecture Notes in Computer Science, pages 36-60. Springer, 2009.
6. S.S. Skiena. The Algorithm Design Manual. Springer Verlag, New York, 1998. Second Printing.