A discussion of how to apply the Cleanroom software development methodology to functional programming using the Haskell language.
Table of Contents
promote.hs: Move matching elements to the front of a list
As my career approaches fifty years in software design, I continue to learn and revise my methods. This paper is a collection of notes on my attempts to learn functional programming with Haskell and how I have modified my technique to accommodate functional thinking.
As part of my crusade for solid connections between the semantics of programs and their mathematical foundations, The Cleanroom software development methodology describes how I apply the Cleanroom methodology to imperative and object-oriented software design. This work is in turn based on the work of my most influential colleague:
I would also like to thank my colleague Daniel Lyons for providing what I think is a quite accessible and well-written yet rigorous and mathematically inclined introduction to Haskell:
Bird, Richard. Thinking functionally with Haskell. Cambridge University Press, 2015, ISBN 978-1-107-45264-0.
I would like to recommend this next work for a relatively quick and painless way to learn Haskell's features:
Lipovača, Miran. Learn you a Haskell for Great Good! No Starch Press, 2011, ISBN 978-1593272838.
The following sections are extended discussions of the questions and examples from these books and from other sources.
Because the Cleanroom methodology requires precise definitions of the semantics of every code block, I've added semantic descriptions using the intended value notation developed in Toward zero-defect programming, especially in §9.4, p. 178.
Generally I follow Stavely's notation for intended values.
However, I prefer to notate preconditions as “
some precondition ...
We notate semantics using lambda-notation, but with
Haskell syntax, as a Haskell line comment starting
--” and enclosed
[…]”. So a
x y . 2*x + y) would
be expressed in our Haskell code as:
-- [ \ x y -> 2*x + y ]
A simple closed interval is written as
[i..j] and denotes the sequence [i, i+1, i+2, ..., j].
An arithmetic progression is written as
[i1,i2..in] and denotes the sequence [i1,
where d ≡
Here are some interactive examples demonstrating Haskell's sequence notation using ghci, the Glasgow Haskell Compiler and Interpreter.
ghci> [3..6] [3,4,5,6] ghci> [10,20..50] [10,20,30,40,50] ghci> [10,20..59] [10,20,30,40,50] ghci> [35,28..0] [35,28,21,14,7,0]
My advice is not to rely on Haskell's
float type for a predictable edge case where
in-i1 is not an
exact multiple of d.
Sometimes the resulting sequence will include numbers