Course description This course offers a 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 such as Z.
The course will develop a purely functional perspective on algorithm specification, 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 plus Edsger W. Dijkstra, "EWD472: Guarded commands, non-determinacy and formal derivation of programs." Instead of formal program derivation, we demonstrate test automation of Hoare style assertions.
Prerequisites
This is an introductory course with no formal prerequisites at all. The introduction will be at a serious speed, while remaining accessible to students with a wide variety of backgrounds. Anyone with a willingness to learn formal methods should be able to follow. Students with some previous experience with (functional) programming will be at an advantage, though.It is a good idea to bring your laptop.
Preparation (for eager students only)
- If you bring a laptop, make sure the Haskell platform is installed on it. See platform.
- You can find chapters 1 and 2 of The Haskell Road to Logic, Maths and Programming under this link.
- Please read Chapters 1 and 2 of "The Haskell Road", and make notes of everything that you do not understand.
- Instead of the Hugs interpreter mentioned in the book, we will use the GHC interpreter, ghci. This interpreter comes with the Haskell platform.
- Note: pattern matching on the pattern
(x+1) is no longer allowed in the new Haskell standard. Therefore, you will get error messages when you want to read in the code for the first Haskell Road chapter in ghci. This can be remedied by changing(x+1) in the head of a definition clause intox , andx in the body of that clause into(x-1) .
Course-outline
- Background: The Haskell Road, Chapters 1 and 2.
- Overview of the course: Overview.
- Course slides for Day 1: Getting Started.
- Code in de slides for Day 1: GettingStarted.hs.
- Exercises for the first day: Exerc1.pdf.
- Code for the exercises for the first day: Exerc1.hs.
- Solutions to exercises for the first day: Answers1.hs.
- Course slides for Day 2: Functional Imperative.
- Code from the course slides for Day 2: FunctionalImperative.hs.
- Course slides for Day 2: Reasoning.
- Code from the course slides for Day 2: Reasoning.hs.
- Exercises for the second day: Exerc2.pdf.
- Code for the exercises for the first day: Exerc2.hs.
- Solutions to exercises for the second day: Answers2.pdf.
- Code for solutions to exercises for the second day: Answers2.hs.
- Course slides for Day 3: AssertiveCoding.
- Code from the course slides for Day 3: AssertiveCoding.hs.
- Modules for assertions: Assert.hs and AssertDoc.hs.
- Module for loops: While.hs.
- Exercises for the third day: Exerc3.pdf.
- Code for exercises for the third day: Exerc3.hs.
- Solutions to exercises for the third day: Answers3.pdf.
- Code for solutions to exercises for the third day: Answers3.hs.
- Course slides for Day 4: GraphsAlgs.
- Code from the course slides for Day 4: GraphsAlgs.hs.
- Exercises for the fourth day: Exerc4.pdf.
- Code for exercises for the fourth day: Exerc4.hs.
- Solutions to exercises for the fourth day: Answers4.
- Code for solutions to exercises for the fourth day: Answers4.hs.
- Course slides for Day 5: MatchingDivision.
- Code from the course slides for Day 5: MatchingDivision.hs.
- Exercises for the fifth day: Exerc5.pdf.
- Code for exercises for the fifth day: Exerc5.hs.
- Solutions to exercises for the fifth day: to be provided.
Monday: Haskell as an Algorithm Specification Language
Tuesday: Functional Imperative Style
Wednesday: Assertive Coding, and Correctness of Algorithms
Thursday: Graph Algorithms
Friday: Algorithms for Matching and Fair Division
Useful links