**Abstract**

A discussion of how to apply the Cleanroom software development methodology to functional programming using the Haskell language.

This publication is available in Web form and also as a PDF document.
Please forward any comments to ** john@nmt.edu**.

This work is licensed under a Creative Commons Attribution-NonCommercial 3.0 Unported License.

**Table of Contents**

- 1. Cleanroom and Haskell: A firm foundation for program semantics
- 2. Notation and composition
- 3. Managing case structures
- 4.
`n2w.hs`

: The`Numbers2Words`

example - 5. Exercises from chapter 1
- 6. Exercises from Chapter 2
- 7. A
`partition`

function - 8. The segment list problem
- 9.
`promote.hs`

: Move matching elements to the front of a list - 10. The permuted folding problem
- 11. Acknowledgements

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 “`P: `

”.
`some precondition ...`

We notate semantics using lambda-notation, but with Haskell syntax, as a Haskell line comment starting with “

`--`

” and enclosed in “`[…]`

”. So a function*(*λ*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*[i*where_{1}, i_{1}+d, i_{1}+2d, ..., i_{n}]*d*≡*i*._{2}- i_{1}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*i*is not an exact multiple of_{n}-i_{1}*d*. Sometimes the resulting sequence will include numbers beyond*i*._{n}