Exploring Languages
with Interpreters
and Functional Programming

Chapter 7
Data 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 Chapter 7, Data Abstraction, in the 2018 version of the textbook Exploring Languages with Interpreters and Functional Programming.

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 modules for the Rational Arithmetic case study are in files RationalCore.hs, RationalDeferGCD.hs, Rational1.hs, and Rational2.hs.

Using Data Abstraction

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

Rational Numbers

Mathematical rational numbers 𝚡𝚢\frac{\texttt{x}}{\texttt{y}} where

Rational Number Abstraction

Rational Arithmetic Operations

Assuming data abstraction (Rat, makeRat, zeroRat, numer, denom)

    negRat :: Rat -> Rat 
    negRat x = makeRat (- numer x) (denom x)

    addRat, subRat, mulRat, divRat :: Rat -> Rat -> Rat
    addRat x y = makeRat (numer x * denom y + numer y * denom x)
                         (denom x * denom y) 
    subRat x y = makeRat (numer x * denom y - numer y * denom x)
                         (denom x * denom y) 
    mulRat x y = makeRat (numer x * numer y) (denom x * denom y) 
    divRat x y  -- (2) (3)
        | eqRat y zeroRat = error "Attempt to divide by 0"
        | otherwise       = makeRat (numer x * denom y)
                                    (denom x * numer y)

    eqRat :: Rat -> Rat -> Bool 
    eqRat x y = (numer x) * (denom y) == (numer y) * (denom x)

Representing Rationals

Rational Representation Prop.

Advantages of Representation

Implementing Rationals (1)

First implement constructor

    makeRat :: Int -> Int -> Rat
    makeRat x 0 = error ( "Cannot construct a rational number "
                          ++ show x ++ "/0" ) 
    makeRat 0 _ = zeroRat
    makeRat x y = (x' `div` d, y' `div` d) 
        where x' = (signum' y) * x  -- (1,2)
              y' = abs' y 
              d  = gcd' x' y'
  1. where clause introduces local definitions x', y', d within makeRat body

  2. type inference for x', y', d — all Int because of makeRat signature

Implementing Rationals (2)

Precondition of makeRat x y

y /= 0

Postcondition of makeRat x y = (x',y')

(x',y') satisfies the Rational Representation Property

Rational number value is 𝚡𝚢\frac{\texttt{x}}{\texttt{y}}

Together postconditions imply 𝚡’𝚢’\frac{\texttt{x'}}{\texttt{y'}} == 𝚡𝚢\frac{\texttt{x}}{\texttt{y}}

Implementing Rationals (3)

    signum' :: Int -> Int      -- similar Prelude signum
    signum' n | n == 0     =  0 
              | n > 0      =  1 
              | otherwise  = -1 

    abs' :: Int -> Int         -- similar Prelude abs
    abs' n | n >= 0    =  n
           | otherwise = -n

    gcd' :: Int -> Int -> Int  -- similar Prelude gcd
    gcd' x y = gcd'' (abs' x) (abs' y) 
        where gcd'' x 0 = x 
              gcd'' x y = gcd'' y (x `rem` y) 

    showRat :: Rat -> String
    showRat x = show (numer x) ++ "/" ++ show (denom x)

Implementing Rationals (4)

    numer, denom :: Rat -> Int
    numer (x,_) = x
    denom (_,y) = y

Preconditions for numer (x,y) and denom (x,y)

Arguments (x,y) satisfy Rational Representation Property

Postconditions for numer (x,y) = x and denom (x,y) = y

𝚗𝚞𝚖𝚎𝚛 (𝚡,𝚢)y\frac{\texttt{numer (x,y)}}{y} == 𝚡𝚢\frac{\texttt{x}}{\texttt{y}} — no change to input

𝚡𝚍𝚎𝚗𝚘𝚖 (𝚡,𝚢)\frac{\texttt{x}}{\texttt{denom (x,y)}} == 𝚡𝚢\frac{\texttt{x}}{\texttt{y}} — no change to input

Modularization

Package has groups of features:

  1. public rational arithmetic functions: negRat, addRat, subRat, mulRat, divRat, eqRat

  2. public type Rat, constant zeroRat, constructor makeRat, selectors numer and denom, string converter showRat

  3. private utility functions used by second group, but just reimplementations of Prelude functions

Module RationalCore

Module Rational (1)

Module Rational (2)

Modularization Critique

Alternative Data Representation

Implementing RationalDeferGCD (1)

    module RationalDeferGCD
        (Rat, zeroRat, makeRat, numer, denom, showRat)
    where

    type Rat = (Int,Int)

    zeroRat :: (Int,Int)
    zeroRat = (0,1)

    makeRat :: Int -> Int -> Rat
    makeRat x 0 = error ( "Cannot construct a rational number "
                          ++ show x ++ "/0" )
    makeRat 0 y = zeroRat 
    makeRat x y = (x,y)

Implementing RationalDeferGCD (2)

    numer :: Rat -> Int
    numer (x,y) = x' `div` d
        where x' = (signum' y) * x 
              y' = abs' y 
              d  = gcd' x' y'

    denom :: Rat -> Int
    denom (x,y) = y' `div` d
        where x' = (signum' y) * x 
              y' = abs' y 
              d  = gcd' x' y'

    showRat :: Rat -> String
    showRat x = show (numer x) ++ "/" ++ show (denom x)
    
    -- signum', abs', gcd' as before

Deferred Representation Prop.

Compare: Allows y < 0, not relatively prime

RationalDeferGCD Contracts (1)

Precondition makeRat x y

y /= 0

Postcondition makeRat x y = (x',y')

(x',y') satisfies the Deferred Representation Property

Rational number value is 𝚡𝚢\frac{\texttt{x}}{\texttt{y}}

RationalDeferGCD Contracts (2)

Precondition numer (x,y) and denom(x,y)

(x,y) satisfies Deferred Representation Property

Postconditions numer (x,y) = x' and denom (x,y) = y

𝚗𝚞𝚖𝚎𝚛 (𝚡,𝚢)y\frac{\texttt{numer (x,y)}}{y'} == 𝚡𝚢\frac{\texttt{x}}{\texttt{y}} — no change to input

𝚡’𝚍𝚎𝚗𝚘𝚖 (𝚡,𝚢)\frac{\texttt{x'}}{\texttt{denom (x,y)}} == 𝚡𝚢\frac{\texttt{x}}{\texttt{y}} — no change to input

If makeRat x y == r, numer r = x', and denom r = y', then postconditions imply that 𝚡’𝚢’\frac{\texttt{x'}}{\texttt{y'}} == 𝚡𝚢\frac{\texttt{x}}{\texttt{y}}

Module RationalDeferGCD

Using RationalDeferGCD

    module Rational2    -- note suffix 2
      ( Rat, zeroRat, makeRat, numer, denom, showRat,
        negRat, addRat, subRat, mulRat, divRat, eqRat )
    where

    import RationalDeferGCD
    -- negRat, addRat, subRat, mulRat, divRat, eqRat definitions
    -- code same as in Rational1

“Abstract” Modules

RationalCore and RationalDeferGCD

Rational1 and Rational2

Rational Number Package

Figure 7-1. Module Dependencies

Figure 7-1. Module Dependencies

Invariants (1)

Invariants assert what must hold for an “object” to be valid

Invariant:
Logical assertion that always holds for every “object” created by public constructors and manipulated only by public operations
Interface invariant:
Invariant stated in terms of public features and abstract properties of “object”
Implementation (representation) invariant:
Detailed invariant giving required relationships among internal features of implementation of “object”

Invariants (2)

RationalRep Interface Invariant

For any valid Haskell rational number r:

r \in Rat

denom r > 0

If numer r == 0, then denom r == 1

numer r and denom r are relatively

Rational number value is 𝚗𝚞𝚖𝚎𝚛 𝚛𝚍𝚎𝚗𝚘𝚖 𝚛\frac{\texttt{numer r}}{\texttt{denom r}}

RationalRep Pre/Postconditions (1)

Abstract interface precondition makeRat x y

y /= 0

Abstract interface postcondition makeRat x y = r

r satisfies the RationalRep Interface Invariant

Rational number r’s value is 𝚡𝚢\frac{\texttt{x}}{\texttt{y}}

RationalRep Pre/Postconditions (2)

Abstract interface precondition numer r and denom r

r satisfies the RationalRep Interface Invariant

Abstract interface postcondition numer r = x' and denom r = y'

Rational number value 𝚡’𝚍𝚎𝚗𝚘𝚖 𝚛\frac{\texttt{x'}}{\texttt{denom r}} equals rational number value of r

Rational number value 𝚗𝚞𝚖𝚎𝚛 𝚛y\frac{\texttt{numer r}}{y'} equals rational number value of r

RationalCore Implementation Inv.

For any valid Haskell rational number r:

r == (x,y) for some (x,y) \in Rat

y > 0

if x == 0, then y == 1

x and y are relatively prime

Rational number value is 𝚡𝚢\frac{\texttt{x}}{\texttt{y}}

Implies interface invariant given RationalCore implementation

RationalDeferGCD Implementation Inv.

For any valid Haskell rational number r:

r == (x,y) for some (x,y) \in Rat

y /= 0

if x == 0, then y == 1

Rational number value is 𝚡𝚢\frac{\texttt{x}}{\texttt{y}}

Implies interface invariant given RationalCore implementation

Other Alternative Representations

Haskell Module System

Testing

Chapter 12 discusses testing of package — test against abstract interface and contracts

Defining Haskell Modules

Key Ideas

Source Code