Exploring Languages
with Interpreters
and Functional Programming
— Section 6.2 —
Using Top-Down Stepwise Refinement
(Procedural Abstraction)

H. Conrad Cunningham

12 September 2018

Copyright (C) 2017, 2018, H. Conrad Cunningham

Acknowledgements: I originally created these slides in Fall 2017 to accompany what is now Section 6.2, Using Top-Down Stepwise Refinement, in the 2018 version of the textbook Exploring Languages with Interpreters and Functional Programming. This is part of Chapter 6, Procedural Abstraction.

Browser Advisory: The HTML version of this document may require use of a browser that supports the display of MathML. A good choice as of September 2018 is a recent version of Firefox from Mozilla.

Code: The Haskell module for the Square root case study is in source file Sqrt.hs. Source file TestSqrt.hs includes some smoke testing code.

Using Top-Down Stepwise Refinement

Lecture Goals

Kinds of Abstraction

  1. Procedural abstraction: separate properties of action from implementation details

    Break complex actions into subprograms; develop program as sequence of calls

  2. Data abstraction: separate properties of data from representation details

    Identify key data representations; develop program around these and associated operations

Square Root Problem

Solution Strategy (1 of 2)

Top-down stepwise refinement – adapt general method to Haskell

Solution Strategy (2 of 2)

High-level Solution (1 of 2)

Postulate function with signature

    sqrtIter :: Double -> Double -> Double 

Encode Newton method step 2

    sqrtIter guess x 
        | goodEnough guess x = guess 
        | otherwise          = sqrtIter (improve guess x) x 

High-level Solution (2 of 2)

    sqrtIter guess x 
        | goodEnough guess x = guess 
        | otherwise          = sqrtIter (improve guess x) x 

Refinement: improve

Refine improve in Newton step 3 – assuming precondition x >= 0 && guess > 0

    improve :: Double -> Double -> Double
    improve guess x = average guess (x/guess)

Refinement: goodEnough

Refine goodEnough

Initial Guess

Sufficient just to use 1

    sqrt' :: Double -> Double
    sqrt' x | x >= 0 = sqrtIter 1 x

Making Haskell Module Sqrt.hs

    module Sqrt -- put in file "Sqrt.hs"
        (sqrt') -- only export sqrt', others hidden
    where

    sqrt' :: Double -> Double
    sqrt' x | x >= 0 = sqrt_iter 1 x

    sqrt_iter :: Double -> Double -> Double
    sqrt_iter guess x
        | good_enough guess x = guess
        | otherwise           = sqrt_iter (improve guess x) x

    good_enough :: Double -> Double -> Bool
    good_enough guess x = abs (square guess - x) < 0.001

    square :: Double -> Double
    square x = x * x

    average :: Double -> Double -> Double
    average x y = (x + y) / 2

    improve :: Double -> Double -> Double
    improve guess x = average guess (x/guess)

Using Haskell Module

Example use of Sqrt module (from TestSqrt.hs)

    module TestSqrt
    where

    import Sqrt -- file Sqrt.hs, import all public features 

    main = do
        putStrLn (show (sqrt' 16))
        putStrLn (show (sqrt' 2))

Key Ideas

Source Code