Next / Previous / Contents / Shipman's homepage

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 BY-NC Creative Commons Attribution-NonCommercial 3.0 Unported License.

Table of Contents

1. Cleanroom and Haskell: A firm foundation for program semantics
1.1. Some Haskell notational conventions
2. Notation and composition
2.1. Simple composition of functions
2.2. Composition with partial application
3. Managing case structures
4. n2w.hs: The Numbers2Words example
4.1. n2w.hs: Prologue
4.2. convert1: Convert single-digit numbers
4.3. convert2: Convert numbers up to 99
4.4. convert3: Convert numbers up to 999
4.5. convert6: Convert numbers less than a million
4.6. n2w.hs: Epilogue
5. Exercises from chapter 1
5.1. Definitions for Exercise A
5.2. Exercise A, first pair
5.3. Exercise A, second pair
5.4. Exercise A, third pair
5.5. Exercise F
6. Exercises from Chapter 2
6.1. Exercise C: modernise
6.2. Exercise G: showDate
7. A partition function
7.1. partition, case A: C1
7.2. partition, case B: C1' & C2
7.3. partition, case C: C1' & C2'
8. The segment list problem
8.1. Segment list design
8.2. seglist.hs: Prologue
8.3. Specification functions
8.4. The Seg data type
8.5. The mergeSegLists() function
8.6. The Python version: seglist.py
9. promote.hs: Move matching elements to the front of a list
9.1. promote.hs: The code
9.2. Verification of the promoteEq function
9.3. Verification of the promote' helper function
9.4. promote': Case A
9.5. promote': Case B
9.6. promote': Case C
10. The permuted folding problem
11. Acknowledgements

1. Cleanroom and Haskell: A firm foundation for program semantics

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:

Stavely, Allan M. Toward zero-defect programming. Addison-Wesley, 1999, ISBN 0-201-38595-3.

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 ...”.

1.1. Some Haskell notational conventions

  • 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 [i1, i1+d, i1+2d, ..., in] where di2 - i1.

    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 beyond in.