\PassOptionsToPackage{unicode=true}{hyperref} % options for packages loaded elsewhere
\PassOptionsToPackage{hyphens}{url}
%
\documentclass[
  english,
]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
  \usepackage{textcomp} % provides euro and other symbols
\else % if luatex or xelatex
  \usepackage{unicode-math}
  \defaultfontfeatures{Scale=MatchLowercase}
  \defaultfontfeatures[\rmfamily]{Ligatures=TeX,Scale=1}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
\IfFileExists{microtype.sty}{% use microtype if available
  \usepackage[]{microtype}
  \UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\makeatletter
\@ifundefined{KOMAClassName}{% if non-KOMA class
  \IfFileExists{parskip.sty}{%
    \usepackage{parskip}
  }{% else
    \setlength{\parindent}{0pt}
    \setlength{\parskip}{6pt plus 2pt minus 1pt}}
}{% if KOMA class
  \KOMAoptions{parskip=half}}
\makeatother
\usepackage{xcolor}
\IfFileExists{xurl.sty}{\usepackage{xurl}}{} % add URL line breaks if available
\IfFileExists{bookmark.sty}{\usepackage{bookmark}}{\usepackage{hyperref}}
\hypersetup{
  pdftitle={CSci 555: Functional Programming Data Abstraction},
  pdfauthor={H. Conrad Cunningham},
  pdfborder={0 0 0},
  breaklinks=true}
\urlstyle{same}  % don't use monospace font for urls
\usepackage{color}
\usepackage{fancyvrb}
\newcommand{\VerbBar}{|}
\newcommand{\VERB}{\Verb[commandchars=\\\{\}]}
\DefineVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\{\}}
% Add ',fontsize=\small' for more characters per line
\newenvironment{Shaded}{}{}
\newcommand{\AlertTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\AnnotationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\AttributeTok}[1]{\textcolor[rgb]{0.49,0.56,0.16}{#1}}
\newcommand{\BaseNTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\BuiltInTok}[1]{#1}
\newcommand{\CharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\CommentTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textit{#1}}}
\newcommand{\CommentVarTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\ConstantTok}[1]{\textcolor[rgb]{0.53,0.00,0.00}{#1}}
\newcommand{\ControlFlowTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\DataTypeTok}[1]{\textcolor[rgb]{0.56,0.13,0.00}{#1}}
\newcommand{\DecValTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\DocumentationTok}[1]{\textcolor[rgb]{0.73,0.13,0.13}{\textit{#1}}}
\newcommand{\ErrorTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\ExtensionTok}[1]{#1}
\newcommand{\FloatTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\FunctionTok}[1]{\textcolor[rgb]{0.02,0.16,0.49}{#1}}
\newcommand{\ImportTok}[1]{#1}
\newcommand{\InformationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\KeywordTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\NormalTok}[1]{#1}
\newcommand{\OperatorTok}[1]{\textcolor[rgb]{0.40,0.40,0.40}{#1}}
\newcommand{\OtherTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{#1}}
\newcommand{\PreprocessorTok}[1]{\textcolor[rgb]{0.74,0.48,0.00}{#1}}
\newcommand{\RegionMarkerTok}[1]{#1}
\newcommand{\SpecialCharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\SpecialStringTok}[1]{\textcolor[rgb]{0.73,0.40,0.53}{#1}}
\newcommand{\StringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\VariableTok}[1]{\textcolor[rgb]{0.10,0.09,0.49}{#1}}
\newcommand{\VerbatimStringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\WarningTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{-2}
% Redefines (sub)paragraphs to behave more like sections
\ifx\paragraph\undefined\else
  \let\oldparagraph\paragraph
  \renewcommand{\paragraph}[1]{\oldparagraph{#1}\mbox{}}
\fi
\ifx\subparagraph\undefined\else
  \let\oldsubparagraph\subparagraph
  \renewcommand{\subparagraph}[1]{\oldsubparagraph{#1}\mbox{}}
\fi

% set default figure placement to htbp
\makeatletter
\def\fps@figure{htbp}
\makeatother

\usepackage{caption}
\DeclareCaptionLabelFormat{nolabel}{}
\captionsetup{labelformat=nolabel}
\ifnum 0\ifxetex 1\fi=0 % if pdftex or luatex
  \usepackage[shorthands=off,main=english]{babel}
\else % if xetex
  % load polyglossia as late as possible as it *could* call bidi if RTL lang (e.g. Hebrew or Arabic)
  \usepackage{polyglossia}
  \setmainlanguage[]{english}
\fi

\title{CSci 555: Functional Programming\\
Data Abstraction}
\author{\textbf{H. Conrad Cunningham}}
\date{\textbf{14 February 2019}}

\begin{document}
\maketitle

{
\setcounter{tocdepth}{4}
\tableofcontents
}
Copyright (C) 2017, 2018, 2019, \href{http://www.cs.olemiss.edu/~hcc}{H.
Conrad Cunningham}\\
Professor of \href{https://www.cs.olemiss.edu}{Computer and Information
Science}\\
\href{http://www.olemiss.edu}{University of Mississippi}\\
211 Weir Hall\\
P.O. Box 1848\\
University, MS 38677\\
(662) 915-5358

\textbf{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 February 2019 is a recent version of Firefox from Mozilla.

TODO: Update the programming language support to be more generic.

\newpage

\hypertarget{data-abstraction}{%
\section{Data Abstraction}\label{data-abstraction}}

\hypertarget{what-is-abstraction}{%
\subsection{What is Abstraction?}\label{what-is-abstraction}}

As computing scientists and computer programmers, we should remember the
maxim:

\begin{quote}
\emph{Simplicity is good; complexity is bad.}
\end{quote}

The most effective weapon that we have in the fight against complexity
is \emph{abstraction}. What is abstraction?

Abstraction is \emph{concentrating on the essentials and ignoring the
details.}

Sometimes abstraction is described as \emph{remembering the ``what'' and
ignoring the ``how''}.

\hypertarget{kinds-of-abstraction}{%
\subsubsection{Kinds of abstraction}\label{kinds-of-abstraction}}

Large complex systems can only be made understandable by decomposing
them into modules. When viewed from the outside, from the standpoints of
users, each \emph{module} should be simple, with the complexity hidden
inside.

We strive for modules that have simple interfaces that can be used
without knowing the implementations. Here we use \emph{interface} to
mean any information about the module that other modules must assume to
be able to do their work correctly.

Two kinds of abstraction are of interest to computing scientists:
\emph{procedural abstraction} and \emph{data abstraction}.

\begin{description}
\tightlist
\item[Procedural abstraction:]
the separation of the logical properties of an \emph{action} from the
details of how the action is implemented.
\item[Data abstraction:]
the separation of the logical properties of \emph{data} from the details
of how the data are represented.
\end{description}

When we develop an algorithm following the top-down approach, we are
practicing procedural abstraction. At a high level, we break the problem
up into several tasks. We give each task a name and state its
requirements, but we do not worry about how the task is to be
accomplished until we expand it at a lower level of our design.

When we code a task in a programming language, we will typically make
each task a subprogram (procedure, function, subroutine, method, etc.).
Any other program component that calls the subprogram needs to know its
interface (name, parameters, return value, assumptions, etc.) but does
not need to know the subprogram's internal implementation details. The
internal implementation can be changed without affecting the caller.

In data abstraction, the focus is on the problem's data rather than the
tasks to be carried out.

\hypertarget{procedures-and-functions}{%
\subsubsection{Procedures and
functions}\label{procedures-and-functions}}

Generally we make the following distinctions among subprograms:

\begin{itemize}
\item
  A \emph{procedure} is (in its pure form) a subprogram that takes zero
  or more arguments but does not return a value. It is executed for its
  effects, such as changing values in a data structure within the
  program, modifying its reference or value-result arguments, or causing
  some effect outside the program (e.g.~displaying text on the screen or
  reading from a file).
\item
  A \emph{function} is (in its pure form) a subprogram that takes zero
  or more arguments and returns a value but that does not have other
  effects.
\item
  A \emph{method} is a procedure or function often associated with an
  object or class in an object-oriented program. Some object-oriented
  languages use the metaphor of message-passing. A method is the feature
  of an object that receives a message. In an implementation, a method
  is typically a procedure or function associated with the (receiver)
  object; the object may be an implicit parameter of the method.
\end{itemize}

Of course, the features of various programming languages and usual
practices for their use may not follow the above pure distinctions. For
example, a language may not distinguish between procedures and
functions. One term or another may be used for all subprograms.
Procedures may return values. Functions may have side effects. Functions
may return multiple values. The same subprogram can sometimes be called
either as a function or procedure.

Nevertheless, it is good practice to maintain the distinction between
functions and procedures for most cases in software design and
programming.

In Haskell, the primary unit of procedural abstraction is the pure
function. Their definitions may be nested within other functions.
Haskell also groups functions and other declarations into a program unit
called a \VERB|\KeywordTok{module}|. A \VERB|\KeywordTok{module}|
explicitly exports selected functions and keep others hidden.

In Java, the primary unit of procedural abstraction is the method, which
may be a procedure, a pure function, or an impure (side-effecting)
function. A method must be part of a Java \VERB|\KeywordTok{class}|,
which is, in turn, part of a Java \VERB|\KeywordTok{package}|.

Scala combines characteristics of Java and Haskell. It has Java-like
methods, which can be nested inside other methods. Scala also has
\VERB|\KeywordTok{class}|, \VERB|\KeywordTok{object}|,
\VERB|\KeywordTok{trait}|, and \VERB|\KeywordTok{package}| constructs
that include procedural abstractions.

\hypertarget{concrete-data-structures}{%
\subsection{Concrete Data Structures}\label{concrete-data-structures}}

In most languages (e.g.~C), data structures are visible. A programmer
can define custom data types, yet their structure and values are known
to other parts of the program. These are \emph{concrete data
structures}.

As an example, consider a collection of records about the employees of a
company. Suppose we store these records in a global C array. The array
and all its elements are visible to all parts of the program. Any
statement in the program can directly access and modify the elements of
the array.

The use of concrete data structures is convenient, but it does not scale
well and it is not robust with respect to change. As a program gets
large, keeping track of the design details of many concrete data
structures becomes very difficult. Also, any change in the design or
implementation of a concrete data structures may require change to all
code that uses it.

\hypertarget{abstract-data-structures}{%
\subsection{Abstract Data Structures}\label{abstract-data-structures}}

An \emph{abstract data structure} is a module consisting of data and
operations. The data are hidden within the module and can only be
accessed by means of the operations. The data structure is called
\emph{abstract} because its name and its interface are known, but not
its implementation. The operations are explicitly given; the values are
only defined implicitly by means of the operations.

An abstract data structure supports \emph{information hiding}. Its
implementation is hidden behind an interface that remains unchanged,
even if the implementation changes. The implementation detail of the
module is a design decision that is kept as a \emph{secret} from the
other modules.

The concept of \emph{encapsulation} is related to the concept of
information hiding. The data and the operations that manipulate the data
are all combined in one place. That is, they are encapsulated within a
module.

An abstract data structure has a \emph{state} that can be manipulated by
the operations. The state is a value, or collection of information, held
by the abstract data structure.

As an example, again consider the collection of records about the
employees of a company. Suppose we impose a discipline on our program,
only allowing the collection of records to be accessed through a small
group of procedures (and functions). Inside this group of procedures,
the array of records can be manipulated directly. However, all other
parts of the program must use one of the procedures in the group to
manipulate the records in the collection. The fact that the collection
is implemented with an array is (according to the discipline we imposed)
hidden behind the interface provided by the group of procedures. It is a
secret of the module providing the procedures.

Now suppose we wish to modify our program and change the implementation
from an array to a linked list or maybe to move the collection to a disk
file. By approaching the design of the collection as an abstract data
structure, we have limited the parts of the program that must be changed
to the small group of procedures that used the array directly; other
parts of the program are not affected.

As another example of an abstract data structure, consider a stack. We
provide operations like \texttt{push}, \texttt{pop}, and \texttt{empty}
to allow a user of the stack to access and manipulate it. Except for the
code implementing these operations, we disallow direct access to the
concrete data structure that implements the stack. The implementation
might use an array, a linked list, or some other concrete data
structure; the actual implementation is ``hidden'' from the user of the
stack.

We, of course, can use the available features of a particular
programming language (e.g.~module, package, class) to hide the
implementation details of the data structure and only expose the access
procedures.

\hypertarget{abstract-data-types}{%
\subsection{Abstract Data Types}\label{abstract-data-types}}

There is only one instance of an abstract data structure. Often we need
to create multiple instances of an abstract data structure. For example,
we might need to have a collection of employee records for each
different department within a large company.

We need to go a step beyond the abstract data structure and define an
\emph{abstract data type} (ADT).

What do we mean by \emph{type}?

\begin{description}
\tightlist
\item[Type:]
a category of entities sharing common characteristics
\end{description}

Consider the built-in type \VERB|\DataTypeTok{int}| in C. By declaring a
C variable to be of type \VERB|\DataTypeTok{int}|, we are specifying
that the variable has the characteristics of that type:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  a value (state) drawn from some set (domain) of possible values---in
  the case of \VERB|\DataTypeTok{int}|, a subset of the mathematical set
  of integers,
\item
  a set of operations that can be applied to those values---in the case
  of \VERB|\DataTypeTok{int}|, addition, multiplication, comparison for
  equality, etc.
\end{enumerate}

Suppose we declare a C variable to have type \VERB|\DataTypeTok{int}|.
By that declaration, we are creating a container in the program's memory
that, at any point in time, holds a single value drawn from the
\VERB|\DataTypeTok{int}| domain. The contents of this container can be
operated upon by the \VERB|\DataTypeTok{int}| operations. In a program,
we can declare several \VERB|\DataTypeTok{int}| variables: each variable
may have a different value, yet all of them have the same set of
operations.

In the definition of a \emph{concrete} data type, the values are the
most prominent features. The values and their representations are
explicitly prescribed; the operations on the values are often left
implicit.

The opposite is the case in the definition of an \emph{abstract} data
type. The operations are explicitly prescribed; the values are defined
implicitly in terms of the operations. A number of representations of
the values may be possible.

Conceptually, an abstract data type is a set of entities whose logical
behavior is defined by a domain of values and a set of operations on
that domain. In the terminology we used above, an ADT is set of abstract
data structures all of whom have the same domain of possible states and
have the same set of operations.

We will refer to a particular abstract data structure from an ADT as an
\emph{instance} of the ADT.

The implementation of an ADT in a language like C is similar to that
discussed above for abstract data structures. In addition to providing
operations to access and manipulate the data, we need to provide
operations to create and destroy instances of the ADT. All operations
(except create) must have as a parameter an identifier (e.g.~a pointer)
for the particular instance to be operated upon.

While languages like C do not directly support ADTs, the
\VERB|\KeywordTok{class}| construct provides a direct way to define ADTs
in languages like C++, Java, and Scala.

\hypertarget{defining-adts}{%
\subsection{Defining ADTs}\label{defining-adts}}

The behavior of an ADT is defined by a set of operations that can be
applied to an \emph{instance} of the ADT.

Each operation of an ADT can have inputs (i.e.~parameters) and outputs
(i.e.~results). The collection of information about the names of the
operations and their inputs and outputs is the \emph{interface} of the
ADT.

To specify an ADT, we need to give:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
  the \emph{name} of the ADT
\item
  the \emph{sets} (or domains) upon which the ADT is built. These
  include the type being defined and the auxiliary types (e.g.~primitive
  data types and other ADTs) used as parameters or return values of the
  operations.
\item
  the \emph{signatures} (syntax or structure) of the operations

  \begin{itemize}
  \tightlist
  \item
    name
  \item
    input sets (i.e.~the types, number, and order of the parameters)
  \item
    output set (i.e.~the type of the return value)
  \end{itemize}
\item
  the \emph{semantics} (or meaning) of the operations
\end{enumerate}

There are two primary approaches for specifying the semantics of the
operations:

\begin{itemize}
\item
  The \emph{axiomatic} (or \emph{algebraic}) approach gives a set of
  logical rules (properties or axioms) that relate the operations to one
  another. The meanings of the operations are defined implicitly in
  terms of each other.
\item
  The \emph{constructive} (or \emph{abstract model}) approach describes
  the meaning of the operations explicitly in terms of operations on
  other abstract data types. The underlying \emph{model} may be any
  well-defined mathematical model or a previously defined ADT.
\end{itemize}

In some ways, the axiomatic approach is the more elegant of the two
approaches. It is based in the well-established mathematical fields of
abstract algebra and category theory. Furthermore, it defines the new
ADT independently of other ADTs. To understand the definition of the new
ADT it is only necessary to understand its axioms, not the semantics of
a model.

However, in practice, the axiomatic approach to specification becomes
very difficult to apply in complex situations. The constructive
approach, which builds a new ADT from existing ADTs, is the more useful
methodology for most practical software development situations.

To illustrate both approaches, let us look at a well-known ADT that we
studied in the introductory data structures course, the stack.

\hypertarget{axiomatic-specification-of-an-unbounded-stack-adt}{%
\subsection{Axiomatic Specification of an Unbounded Stack
ADT}\label{axiomatic-specification-of-an-unbounded-stack-adt}}

In this section we give an axiomatic specification of an unbounded stack
ADT. By unbounded, we mean that there is no maximum capacity for the
number of items that can be pushed onto an instance of a stack.

Remember that an ADT specification consists of the name, sets,
signatures, and semantics.

\hypertarget{name}{%
\subsubsection{Name}\label{name}}

\texttt{Stack} (of \texttt{Item})

In this specification, we are defining an ADT named \texttt{Stack}. The
parameter \texttt{Item} represents the arbitrary unspecified type for
the entities stored in the stack. \texttt{Item} is a formal
\emph{generic parameter} of the ADT specification. \texttt{Stack} is
itself a generic ADT; a different ADT is specified for each possible
\emph{generic argument} that can be substituted for \texttt{Item}.

\hypertarget{sets}{%
\subsubsection{Sets}\label{sets}}

The sets (domains) involved in the \texttt{Stack} ADT are the following:

\begin{description}
\tightlist
\item[\texttt{Stack}:]
the set of all stack instances

(This is the set we are defining with the ADT.)
\item[\texttt{Item}:]
the set of all items that can appear in a stack instance
\item[\texttt{boolean}:]
the primitive Boolean type \texttt{\{\ False,\ True\ \}}
\end{description}

\hypertarget{signatures}{%
\subsubsection{Signatures}\label{signatures}}

To specify the signatures for the operations, we use the notation for
mathematical functions. By a tuple like \texttt{(Stack,\ Item)}, we mean
the Cartesian product of sets \texttt{Stack} and \texttt{Item}, that is,
the set of ordered pairs where the first component is from
\texttt{Stack} and the second is from \texttt{Item}. The set to the
right of the \texttt{-\textgreater{}} is the return type of the
function.

We categorize the operations into one of four groups depending upon
their functionality:

\begin{itemize}
\item
  A \emph{constructor} (sometimes called a creator, factory, or producer
  function) constructs and initializes an instance of the ADT.
\item
  A \emph{mutator} (sometimes called a modifier, command, or ``setter''
  function) returns the instance with its state changed.
\item
  An \emph{accessor} (sometimes called an observer, query, or ``getter''
  function) returns information from the state of an instance without
  changing the state.
\item
  A \emph{destructor} destroys an instance of the ADT.
\end{itemize}

We will normally list the operations in that order.

For now, we assume that a mutator returns a distinct new instance of the
ADT with a state that is a modified version of the original instance's
state. That is, we are taking an applicative (or functional or
referentially transparent) approach to ADT specifications.

Technically speaking, a destructor is not an operation of the ADT. We
can represent the other types of operations as functions on the sets in
the specification. However, we cannot define a destructor in that way.
But destructors are of pragmatic importance in the implementation of
ADTs, particularly in languages that do not have automatic storage
reclamation (i.e.~garbage collection).

The signatures of the \texttt{Stack} ADT operations are as follows.

\hypertarget{constructors}{%
\paragraph{Constructors}\label{constructors}}

\texttt{create:\ \ -\textgreater{}\ Stack}

\hypertarget{mutators}{%
\paragraph{Mutators}\label{mutators}}

\texttt{push:\ (Stack,\ Item)\ -\textgreater{}\ Stack}

\texttt{pop:\ Stack\ -\textgreater{}\ Stack}

\hypertarget{accessors}{%
\paragraph{Accessors}\label{accessors}}

\texttt{top:\ Stack\ -\textgreater{}\ Item}

\texttt{empty:\ Stack\ -\textgreater{}\ boolean}

\hypertarget{destructors}{%
\paragraph{Destructors}\label{destructors}}

\texttt{destroy:\ Stack\ -\textgreater{}}

The operation \texttt{pop} may not be the same as the ``pop'' operation
you learned in a data structures class. The traditional ``pop'' both
removes the top element from the stack and returns it. In this ADT, we
have separated out the ``return top'' functionality into accessor
operation \texttt{top} and left operation \texttt{pop} as a pure mutator
operation that returns the modified stack.

The separation of the traditional ``pop'' into two functions has two
advantages:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  It results in an elegant, applicative stack specification whose
  operations fit cleanly into the mutator/accessor categorization.
\item
  It results in a simpler, cleaner abstraction in which the set of
  operations is ``atomic''. No operation in the ADT's interface can be
  decomposed into other operations also in the interface.
\end{enumerate}

Also note that operation \texttt{destroy} does not return a value. As we
pointed out above, the \texttt{destroy} operation is not really a part
of the formal ADT specification.

\hypertarget{semantics-axiomatic-approach}{%
\subsubsection{Semantics (axiomatic
approach)}\label{semantics-axiomatic-approach}}

We can specify the semantics of the \texttt{Stack} ADT with the
following axioms. Each axiom must hold for all instances \texttt{s} of
type \texttt{Stack} and all entities \texttt{x} of type \texttt{Item}.

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
  \texttt{top(push(s,x))\ =\ x}
\item
  \texttt{pop(push(s,x))\ =\ s}
\item
  \texttt{empty(create())\ =\ True}
\item
  \texttt{empty(push(s,x))\ =\ False}
\end{enumerate}

The axioms are logical assertions that must always be true. Thus we can
write Axioms 3 and 4 more simply as:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\setcounter{enumi}{2}
\tightlist
\item
  \texttt{empty(create())}
\item
  \texttt{not\ empty(push(s,x))}
\end{enumerate}

The first two axioms express the last-in-first-out (LIFO) property of
stacks. Axiom 1 tells us that the top element of the stack is the last
element pushed. Axiom 2 tells us that removal of the top element returns
the stack to the state it had before the last push.

Moreover, axioms 1 and 2 specify the LIFO property of stacks in purely
mathematical terms; there was no need to use the properties of any
representation or use any time-based (i.e.~imperative) reasoning.

The last two axioms define when a stack is empty and when it not. Axiom
3 tells us that a newly created stack is empty. Axiom 4 tells us that
pushing an entity on a stack results in a nonempty stack.

But what about the sequences of operations \texttt{top(create())} and
\texttt{pop(create())}?

Clearly we do not want to allow either \texttt{top} or \texttt{pop} to
be applied to an empty stack. That is, \texttt{top} and \texttt{pop} are
undefined when their arguments are empty stacks.

Functions may be either total or partial.

\begin{itemize}
\item
  A \emph{total} function \texttt{A\ -\textgreater{}\ B} is defined for
  all elements of \texttt{A}.

  For example, the multiplication operation on the set of real numbers
  \texttt{R} is a total function \texttt{(R,R)\ -\textgreater{}\ R}.
\item
  A \emph{partial} function \texttt{A\ -\textgreater{}\ B} is undefined
  for one or more elements of \texttt{A}.

  For example, the division operation on the set of real numbers
  \texttt{R} is a partial function because it is undefined when the
  divisor is \texttt{0}.
\end{itemize}

In software development (and, hence, in specification of ADTs), partial
functions are common. To avoid errors in execution of such functions, we
need to specify the actual domain of the partial functions precisely.

In an axiomatic specification of an ADT, we restrict operations to their
domains by using preconditions. The \emph{precondition} of an operation
is a logical assertion that specifies the assumptions about and the
restrictions upon the values of the arguments of the operation.

If the precondition of an operation is false, then the operation cannot
be safely applied. If any operation is called with its precondition
false, then the program is \emph{incorrect}.

In the axiomatic specification of the stack, we introduce two
preconditions as follows.

\begin{description}
\tightlist
\item[Precondition of \texttt{pop(Stack\ S)}:]
\texttt{not\ empty(S)}
\item[Precondition of \texttt{top(Stack\ S)}]
\texttt{not\ empty(S)}
\end{description}

Note that we have not given the semantics of the destructor operation
\texttt{destroy}. This operation cannot be handled in the simple
framework we have established.

Operation \texttt{destroy} is really an operation on the ``environment''
that contains the stack. By introducing, the ``environment'' explicitly
into our specification, we could specify its behavior more precisely. Of
course, the semantics of \texttt{create} would also need to be extended
to modify the environment and the other operations would likely require
preconditions to ensure that the stack has been created in the
environment.

Another simplification that we have made in this ADT specification is
that we did not impose a bound on the capacity of the stack instance. We
could specify this, but it would also complicate the axioms the
specification.

\hypertarget{constructive-specification-of-a-bounded-stack-adt}{%
\subsection{Constructive Specification of a Bounded Stack
ADT}\label{constructive-specification-of-a-bounded-stack-adt}}

In this section, we give a constructive specification of a bounded stack
ADT. By bounded, we mean that there is a maximum capacity for the number
of items that can be pushed onto an instance of a stack.

\hypertarget{name-1}{%
\subsubsection{Name}\label{name-1}}

\texttt{StackB} (of \texttt{Item})

\hypertarget{sets-1}{%
\subsubsection{Sets}\label{sets-1}}

In this specification of bounded stacks, we have one additional set
involved, the set of integers.

\begin{description}
\tightlist
\item[\texttt{StackB}:]
the set of all stack instances
\item[\texttt{Item}:]
set of all items that can appear in a stack instance
\item[\texttt{boolean}:]
the primitive Boolean type
\item[\texttt{integer}:]
the primitive integer type
\texttt{\{\ ...,\ -2,\ -1,\ 0,\ 1,\ 2,\ ...\ \}}
\end{description}

\hypertarget{signatures-1}{%
\subsubsection{Signatures}\label{signatures-1}}

In this specification of unbounded stacks, we define the \texttt{create}
operation to take the maximum capacity as its parameter.

\hypertarget{constructors-1}{%
\paragraph{Constructors}\label{constructors-1}}

\texttt{create:\ \ integer\ -\textgreater{}\ StackB}

\hypertarget{mutators-1}{%
\paragraph{Mutators}\label{mutators-1}}

\texttt{push:\ (StackB,\ Item)\ -\textgreater{}\ StackB}

\texttt{pop:\ StackB\ -\textgreater{}\ StackB}

In this specification, we add operation \texttt{full} to detect whether
or not the stack instance has reached its maximum capacity.

\hypertarget{accessors-1}{%
\paragraph{Accessors}\label{accessors-1}}

\texttt{top:\ StackB\ -\textgreater{}\ Item}

\texttt{empty:\ StackB\ -\textgreater{}\ boolean}

\texttt{full:\ StackB\ -\textgreater{}\ boolean}

\hypertarget{destructors-1}{%
\paragraph{Destructors}\label{destructors-1}}

\texttt{destroy:\ StackB\ -\textgreater{}}

\hypertarget{semantics-constructive-approach}{%
\subsubsection{Semantics (constructive
approach)}\label{semantics-constructive-approach}}

In the constructive approach, we give the semantics of each operation by
associating both a precondition and a postcondition with the operation.

As before, the \emph{precondition} is a logical assertion that specifies
the required characteristics of the values of the arguments.

A \emph{postcondition} is a logical assertion that specifies the
characteristics of the result computed by the operation with respect to
the values of the arguments.

In the specification in this subsection, we are a bit informal about the
nature of the underlying model. Although the presentation here is
informal, we try to be precise in the statement of the pre- and
postconditions.

Note: We can formalize the model using an ordered pair of type
\texttt{(integer\ max,\ sequence\ stkseq)}, in which \texttt{max} is the
upper bound on the stack size and \texttt{stkseq} is a sequence that
represents the current sequence elements of elements in the stack. This,
more formal alternative, is presented in the next subsection.

\hypertarget{constructor}{%
\paragraph{Constructor}\label{constructor}}

\texttt{create(integer\ size)\ -\textgreater{}\ StackB\ S\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{size\ \textgreater{}=\ 0}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{S\textquotesingle{}} is a valid new instance of
  \texttt{StackB} \&\&

  \texttt{S\textquotesingle{}} has the capacity to store \texttt{size}
  items \&\&

  \texttt{empty(S\textquotesingle{})}
  \end{description}
\end{itemize}

\hypertarget{mutators-2}{%
\paragraph{Mutators}\label{mutators-2}}

\texttt{push(StackB\ S,\ Item\ I)\ -\textgreater{}\ StackB\ S\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S} is a valid \texttt{StackB} instance \&\&

  \texttt{not\ full(S)}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{S\textquotesingle{}} is a valid \texttt{StackB} instance \&\&

  \texttt{S\textquotesingle{}\ =\ S} with \texttt{I} added as the new
  top.
  \end{description}
\end{itemize}

\texttt{pop(StackB\ S)\ -\textgreater{}\ StackB\ S\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S} is a valid \texttt{StackB} instance \&\&

  \texttt{not\ empty(S)}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{S\textquotesingle{}} is a valid \texttt{StackB} instance \&\&

  \texttt{S\textquotesingle{}\ =\ S} with the top item deleted
  \end{description}
\end{itemize}

\hypertarget{accessors-2}{%
\paragraph{Accessors}\label{accessors-2}}

\texttt{top(StackB\ S)\ -\textgreater{}\ Item\ I}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S} is a valid \texttt{StackB} instance \&\&

  \texttt{not\ empty(S)}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{I\ =} the top item on \texttt{S}

  (\texttt{S} is not modified by this operation.)
  \end{description}
\end{itemize}

\texttt{empty(StackB\ S)\ -\textgreater{}\ boolean\ e}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S} is a valid \texttt{StackB} instance
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{e} is \texttt{true} if and only if \texttt{S} contains no
  elements (i.e.~is empty)

  (\texttt{S} is not modified by this operation.)
  \end{description}
\end{itemize}

\texttt{full(StackB\ S)\ -\textgreater{}\ boolean\ f}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S} is a valid \texttt{StackB} instance
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{f} is \texttt{true} if and only if \texttt{S} contains no
  space for additional items (i.e.~is full)

  (\texttt{S} is not modified by this operation.)
  \end{description}
\end{itemize}

\hypertarget{destructor}{%
\paragraph{Destructor}\label{destructor}}

\texttt{destroy(StackB\ S)\ -\textgreater{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S} is a valid \texttt{StackB} instance
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{StackB\ S} no longer exists
  \end{description}
\end{itemize}

Note that each operation except the constructor (\texttt{create}) has a
\texttt{StackB} instance as an input; the constructor and each of the
mutators also has a \texttt{StackB} instance as an output. This
parameter identifies the particular instance that the operation is
manipulating.

Also note that all of these \texttt{StackB} instances are required to be
``valid'' in all preconditions and postconditions, except the
precondition of the constructor and the postcondition of the destructor.
By valid we mean that the state of the instance is within the acceptable
domain of values; it has not become corrupted or inconsistent. What is
specifically mean by ``valid'' will differ from one implementation of a
stack to another.

Suppose we implement the mutator operations as imperative commands
rather then applicative functions. That is, we implement mutators so
that they directly modify the state of an instance instead of returning
a modified copy. (\texttt{S} and \texttt{S\textquotesingle{}} are
implemented as different states of the same physical instance.)

Then, in some sense, the above ``validity'' property is \emph{invariant}
for an instance of the ADT; the constructor makes the property true, all
mutators and accessors preserve its truth, and the destructor makes it
false.

An invariant property must hold between operations on the instance; it
might not hold during the execution of an operation. (For this
discussion, we assume that only one thread has access to the ADT
implementation.)

Aside: An invariant on an ADT instance is similar in concept to an
invariant for a while-loop. A loop invariant holds before and after each
execution of the loop.

As a convenience in specification we will sometimes state the invariants
of the ADT separately from the pre- and postconditions of the methods.
We sometimes will divide the invariants into two groups.

\begin{description}
\tightlist
\item[\emph{interface invariants}:]
invariants stated in terms of publicly accessible features and abstract
properties of the ADT instance.
\item[\emph{implementation (representation) invariants}:]
detailed invariants giving the required relationships among the internal
data fields of the implementation.
\end{description}

The interface invariants are part of the public interface of the ADT.
They only deal with the state of an instance in terms of the abstract
model for the ADT.

The implementation invariants are part of the hidden state of an
instance; in some cases, they define the meaning of the abstract
properties stated in the interface invariants in terms of hidden values
in the implementation.

\hypertarget{more-formal-semantics-for-bounded-stack}{%
\subsubsection{More formal semantics for bounded
stack}\label{more-formal-semantics-for-bounded-stack}}

Let the bounded stack \texttt{StackB} be represented by an ordered pair
of type \texttt{(integer\ max,\ sequence\ stkseq)}, in which
\texttt{max} is the upper bound on the stack size and \texttt{stkseq} is
a sequence that represents the current sequence elements of elements in
the stack.

\hypertarget{constructor-1}{%
\paragraph{Constructor}\label{constructor-1}}

\texttt{create(integer\ size)\ -\textgreater{}\ StackB\ S\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{size\ \textgreater{}=\ 0}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{S\textquotesingle{}\ ==\ (size,{[}{]})}
  \end{description}

  Here \texttt{{[}{]}} represents an empty sequence. The value of a
  variable occurring in the postcondition is the same as that variable's
  value in the precondition.
\end{itemize}

\hypertarget{mutators-3}{%
\paragraph{Mutators}\label{mutators-3}}

\texttt{push(StackB\ S,\ Item\ I)\ -\textgreater{}\ StackB\ S\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S\ ==\ (m,ss)\ \&\&\ m\ \textgreater{}=\ 0\ \&\&\ length(ss)\ \textless{}\ m}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{S\textquotesingle{}\ ==\ (m,{[}I{]}++ss)}
  \end{description}

  Above \texttt{++} denotes the concatenation of its left and right
  operand sequences. The result sequence has all the values from the
  left operand sequence, in the same order, followed by all the values
  from the right operand sequence, in the same order. Also the notation
  \texttt{{[}I{]}} represents a sequence consisting a single element
  with the value \texttt{I}.
\end{itemize}

\texttt{pop(StackB\ S)\ -\textgreater{}\ StackB\ S\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S\ ==\ (m,ss)\ \&\&\ m\ \textgreater{}=\ 0\ \&\&\ length(ss)\ \textgreater{}\ 0}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{S\textquotesingle{}\ ==\ (m,tail(ss))}
  \end{description}

  Above \texttt{tail} is a function that returns the sequence remaining
  after removing the first element of its nonempty sequence argument.
  Similarly, the function \texttt{head} (used below) returns the first
  element of its nonempty sequence argument.
\end{itemize}

\hypertarget{accessors-3}{%
\paragraph{Accessors}\label{accessors-3}}

\texttt{top(StackB\ S)\ -\textgreater{}\ Item\ I}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S\ ==\ (m,ss)\ \&\&\ m\ \textgreater{}=\ 0\ \&\&\ length(ss)\ \textgreater{}\ 0}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{I\ =\ head(ss)\ \&\&\ S\textquotesingle{}\ ==\ S}
  \end{description}
\end{itemize}

\texttt{empty(StackB\ S)\ -\textgreater{}\ boolean\ e}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S\ ==\ (m,ss)\ \&\&\ m\ \textgreater{}=\ 0\ \&\&\ length(ss)\ \textless{}=\ m}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{e\ ==\ (length(ss)\ ==\ 0)\ \ \&\&\ S\textquotesingle{}\ ==\ S}
  \end{description}
\end{itemize}

\texttt{full(StackB\ S)\ -\textgreater{}\ boolean\ f}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S\ ==\ (m,ss)\ \&\&\ m\ \textgreater{}=\ 0\ \ \&\&\ length(ss)\ \textless{}=\ m}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{f\ ==\ (length(ss)\ ==\ m)\ \&\&\ S\textquotesingle{}\ ==\ S}
  \end{description}
\end{itemize}

\hypertarget{destructor-1}{%
\paragraph{Destructor}\label{destructor-1}}

\texttt{destroy(StackB\ S)\ -\textgreater{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{S\ ==\ (m,ss)\ \&\&\ m\ \textgreater{}=\ 0\ \ \&\&\ length(ss)\ \ \ \textless{}=\ m}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{StackB\ S} no longer exists
  \end{description}
\end{itemize}

Using this abstract model, we can state an interface invariant:

\begin{quote}
For a \texttt{StackB\ S}, there exists an integer \texttt{m} and
sequence of \texttt{Item} elements \texttt{l} such that
\texttt{S\ ==\ (m,ss)\ \&\&\ m\ \textgreater{}=\ 0\ \&\&\ length(ss)\ \textless{}=\ m}
\end{quote}

For discussion of implementing ADTs as Java classes, see the
\href{DataAbstraction_Java_ADTs.html}{supplementary notes}. A Java
implementation of the
\href{DataAbstraction_Java_ADTs.html\#java-implementation-of-bounded-stack}{StackB
ADT} appears in those notes.

\hypertarget{date-day-adt}{%
\subsection{Date (Day) ADT}\label{date-day-adt}}

Consider an ADT for storing and manipulating calendar dates. We call the
ADT \texttt{Day} to avoid confusion with the \VERB|\BuiltInTok{Date}|
class in the Java API. This ADT is based on the \VERB|\NormalTok{Day}|
class defined in Chapter 4 of the book {[}Horstmann 1999{]}.

Logically, a calendar date consists of three pieces of information: a
\emph{year} designator, a \emph{month} designator, and a \emph{day} of
the month designator. A secondary piece of information is the day of the
week. In this ADT interface definition, we use integers (e.g.~Java
\VERB|\DataTypeTok{int}|) to designate these pieces of information.

Caveat: The discussion of Java in these notes does not use generic type
parameters.

\hypertarget{constructor-2}{%
\subsubsection{Constructor}\label{constructor-2}}

\texttt{create(integer\ y,\ integer\ m,\ integer\ d)\ -\textgreater{}\ Day\ D\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:
  \texttt{y\ !=\ 0\ \&\&\ 1\ \textless{}=\ m\ \textless{}=\ 12\ \&\&\ 1\ \textless{}=\ d\ \textless{}=\ \#days\ in\ month\ m}
  \&\&]
  \texttt{(y,m,d)} does not fall in the gap formed by the change to the
  modern (Gregorian) calendar
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{D\textquotesingle{}} is a valid new instance of \texttt{Day}
  with year \texttt{y}, month \texttt{m}, and day \texttt{d}
  \end{description}
\end{itemize}

\hypertarget{mutators-4}{%
\subsubsection{Mutators}\label{mutators-4}}

\texttt{setDay(Day\ D,\ integer\ y,\ integer\ m,\ integer\ d)\ -\textgreater{}\ Day\ D\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} is a valid instance of \texttt{Day} \&\&
  \texttt{y\ !=\ 0\ \&\&\ 1\ \textless{}=\ m\ \textless{}=\ 12\ \&\&\ 1\ \textless{}=\ d\ \textless{}=\ \#days\ in\ month}
  \&\&

  \texttt{(y,m,d)} does not fall in the gap formed by the change to the
  modern (Gregorian) calendar
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{D\textquotesingle{}} is a valid instance of \texttt{Day} \&\&

  \texttt{D\textquotesingle{}=\ D} except with year \texttt{y}, month
  \texttt{m}, and day \texttt{d}
  \end{description}

  Question: Should we include \texttt{setDay}, \texttt{setMonth}, and
  \texttt{setYear} operations? What problems might arise?
\end{itemize}

\texttt{advance(Day\ D,\ integer\ n)\ -\textgreater{}\ Day\ D\textquotesingle{}}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} is a valid instance of \texttt{Day}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{D\textquotesingle{}} is a valid instance of \texttt{Day} \&\&

  \texttt{D\textquotesingle{}\ =\ D} with the date moved \texttt{n} days
  later (Negative \texttt{n} moves to an earlier date.)
  \end{description}
\end{itemize}

\hypertarget{accessors-4}{%
\subsubsection{Accessors}\label{accessors-4}}

\texttt{getDay(Day\ D)\ -\textgreater{}\ integer\ d}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} is a valid instance of \texttt{Day}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{d} is day of the month from \texttt{D}, where
  \texttt{1\ \textless{}=\ d\ \textless{}=\ \#days\ in\ month\ getMonth(D)}

  (\texttt{D} is unchanged.)
  \end{description}
\end{itemize}

\texttt{getMonth(Day\ D)\ -\textgreater{}\ integer\ m}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} is a valid instance of \texttt{Day}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{m} is the month from \texttt{D}, where
  \texttt{1\ \textless{}=\ m\ \textless{}=\ 12}

  (\texttt{D} is unchanged.)
  \end{description}
\end{itemize}

\texttt{getYear(Day\ D)\ -\textgreater{}\ integer\ y}

\begin{itemize}
\item
  Precondition: : \texttt{D} is a valid instance of \texttt{Day}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{y} is the year from \texttt{D}, where \texttt{y\ !=\ 0}

  (\texttt{D} is unchanged.)
  \end{description}
\end{itemize}

\texttt{getWeekday(Day\ D)\ -\textgreater{}\ integer\ wd}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} is a valid instance of \texttt{Day}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{wd} is the day of the week upon which \texttt{D} falls: 0 =
  Sunday, 1 = Monday, \ldots, 6 = Saturday

  (\texttt{D} is unchanged.)
  \end{description}
\end{itemize}

\texttt{equals(Day\ D,\ Day\ D1)\ -\textgreater{}\ boolean\ eq}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} and \texttt{D\textquotesingle{}} are valid instances of
  \texttt{Day}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{eq} is true if and only if \texttt{D} and
  \texttt{D\textquotesingle{}} denote the same calendar date

  (\texttt{D} and \texttt{D\textquotesingle{}} are unchanged.)
  \end{description}
\end{itemize}

\texttt{daysBetween(Day\ D,\ Day\ D1)\ -\textgreater{}\ integer\ d}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} and \texttt{D\textquotesingle{}} are valid instances of
  \texttt{Day}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{d} is the number of calendar days from \texttt{D1} to
  \texttt{D}, i.e. \texttt{equals(D,advance(D1,d))} would be true

  (\texttt{D} is unchanged.)
  \end{description}
\end{itemize}

\texttt{toString(Day\ D)\ -\textgreater{}\ String\ s}

\begin{itemize}
\item
  \begin{description}
  \tightlist
  \item[Precondition:]
  \texttt{D} is a valid instance of \texttt{Day}
  \end{description}
\item
  \begin{description}
  \tightlist
  \item[Postcondition:]
  \texttt{s} is the date \texttt{D} expressed in the format
  ``Day{[}\texttt{getYear(D)},\texttt{getMonth(D)},\texttt{getDay(D)}{]}''.

  (\texttt{D} is unchanged.)
  \end{description}
\end{itemize}

Note: This method is a ``standard'' method that should be defined for
most Java classes so that they fit well into the Java language
framework.

\hypertarget{destructor-2}{%
\subsubsection{Destructor}\label{destructor-2}}

\texttt{destroy(Day\ D)\ -\textgreater{}}

\begin{itemize}
\item
  Precondition: \texttt{D} is a valid instance of \texttt{Day}
\item
  Postcondition: \texttt{D} no longer exists
\end{itemize}

A Java implementation of the
\href{DataAbstraction_Java_ADTs.html\#java-class-implementation-for-day-1}{Day
ADT} appears in the supplementary notes.

\hypertarget{client-supplier-relationship}{%
\subsection{Client-Supplier
Relationship}\label{client-supplier-relationship}}

The design and implementation of ADTs (i.e.~classes) must be approached
from two points of view simultaneously:

\begin{description}
\tightlist
\item[\emph{supplier}]
the developers of the ADT --- the providers of the services
\item[\emph{client}]
the users of the ADT --- the users of the services (e.g.~the designers
of other ADTs)
\end{description}

The \emph{client-supplier relationship} is as represented in the
following diagram:

\begin{verbatim}
  ________________             ________________ 
  |                |           |                |
  |     Client     |===USES===>|    Supplier    |
  |________________|           |________________|

     (ADT user)                    (ADT)  
\end{verbatim}

The supplier's concerns include:

\begin{itemize}
\tightlist
\item
  efficient and reliable algorithms and data structures,
\item
  convenient implementation,
\item
  easy maintenance.
\end{itemize}

The clients' concerns include:

\begin{itemize}
\tightlist
\item
  accomplishing their own tasks,
\item
  using the supplier ADT without effort to understand its internal
  details,
\item
  having a sufficient, but not overwhelming, set of operations.
\end{itemize}

As we have noted previously, the \emph{interface} of an ADT is the set
of features (i.e.~public operations) provided by a supplier to clients.

A precise description of a supplier's interface forms a \emph{contract}
between clients and supplier.

The client-supplier contract:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  gives the responsibilities of the client. These are the conditions
  under which the supplier must deliver results --- when the
  \emph{preconditions} of the operations are satisfied (i.e.~the
  operations are called correctly).
\item
  gives the responsibilities of the supplier. These are the benefits the
  supplier must deliver --- make the \emph{postconditions} hold at the
  end of the operation (i.e.~the operations deliver the correct
  results).
\end{enumerate}

The contract

\begin{itemize}
\item
  protects the client by specifying how much must be done by the
  supplier.
\item
  protects the supplier by specifying how little is acceptable to the
  client.
\end{itemize}

If we are both the clients and suppliers in a design situation, we
should consciously attempt to separate the two different areas of
concern, switching back and forth between our supplier and client
``hats''.

\hypertarget{design-criteria-for-adt-interfaces}{%
\subsection{Design Criteria for ADT
Interfaces}\label{design-criteria-for-adt-interfaces}}

We can use the following design criteria for evaluating ADT interfaces.
Of course, some of these criteria conflict with one another; a designer
must carefully balance the criteria to achieve a good interface design.

In object-oriented languages, these criteria also apply to class
interfaces.

\begin{itemize}
\item
  \textbf{Cohesion:} All operations must logically fit together to
  support a single, coherent purpose. The ADT should describe a single
  abstraction.
\item
  \textbf{Simplicity:} Avoid needless features. The smaller the
  interface the easier it is to use the ADT (class).
\item
  \textbf{No redundancy:} Avoid offering the same service in more than
  one way; eliminate redundant features.
\item
  \textbf{Atomicity:} Do not combine several operations if they are
  needed individually. Keep independent features separate. All
  operations should be \emph{primitive}, that is, not be decomposable
  into other operations also in the public interface.
\item
  \textbf{Completeness:} All primitive operations that make sense for
  the abstraction should be supported by the ADT (class).
\item
  \textbf{Consistency:} Provide a set of operations that are internally
  consistent in

  \begin{itemize}
  \tightlist
  \item
    naming convention (e.g.~in use of prefixes like ``set'' or ``get'',
    in capitalization, in use of verbs/nouns/adjectives),
  \item
    use of arguments and return values (e.g.~order and type of
    arguments),
  \item
    behavior (i.e.~make operations work similarly).
  \end{itemize}

  Avoid surprises and misunderstandings. Consistent interfaces make it
  easier to understand the rest of a system if part of it is already
  known.
\item
  \textbf{Reusability:} Do not customize ADTs (classes) to specific
  clients, but make them general enough to be reusable in other
  contexts.
\item
  \textbf{Robustness with respect to modifications:} Design the
  interface of an ADT (class) so that it remains stable even if the
  implementation of the ADT changes.
\item
  \textbf{Convenience:} Where appropriate, provide additional operations
  (e.g.~beyond the complete primitive set) for the convenience of users
  of the ADT (class). Add convenience operations only for frequently
  used combinations after careful study.
\end{itemize}

\hypertarget{conclusion}{%
\subsection{Conclusion}\label{conclusion}}

TODO

\hypertarget{exercises}{%
\subsection{Exercises}\label{exercises}}

TODO

\hypertarget{acknowledgements}{%
\subsection{Acknowledgements}\label{acknowledgements}}

In Spring 2017 I adapted these lecture notes from my previous notes on
this topic. The material here is based, in part, on the presentations in
the books {[}Dale 1996{]}, {[}Horstmann 1995{]}, {[}Horstmann 1999{]},
{[}Meyer 1997{]}, {[}Mossenbock 1995{]}, and {[}Thomas 1995{]}.

I wrote the first version of these lecture notes to use in the first
Java-based version of CSci 211 (then titled File Systems) during Fall
1996. I revised the notes incrementally over the next decade for use in
my Java-based courses on object-orientation and software architecture. I
partially revised the notes for use in my Scala-based classes beginning
in Fall 2008.

In Fall 2013 I updated these notes to better support classes using
non-JVM languages such as Lua, Elixir, and Haskell. I moved the
extensive Java-based content to a separate document and developed
separate case studies for the other languages.

In Summer 2017, I adapted the notes to use Pandoc. I continued to revise
the structure and text in minor ways in 2017, 2018, and 2019.

I incorporated quite a bit of this material in Chapters 2, 6, and 7 of
the 2018 draft of the textbook \emph{Exploring Languages with
Interpreters and Functional Programming}.

I maintain these notes as text in Pandoc's dialect of Markdown using
embedded LaTeX markup for the mathematical formulas and then translate
the notes to HTML, PDF, and other forms as needed.

\hypertarget{references}{%
\subsection{References}\label{references}}

\begin{description}
\tightlist
\item[{[}Dale 1996{]}:]
Nell Dale and Henry M. Walker. \emph{Abstract Data Types:
Specifications, Implementations, and Applications}, D. C. Heath, 1996.
\item[{[}Horstmann 1995{]}:]
Cay S. Horstmann. \emph{Mastering Object-Oriented Design in C++}, Wiley,
1995.
\item[{[}Horstmann 1999{]}:]
Cay S. Horstmann and Gary Cornell, \emph{Core Java 1.2: Volume I --
Fundamentals}, Fourth Edition, Sun Microsystems Press/Prentice Hall,
1999.
\item[{[}Meyer 1997{]}:]
Bertrand Meyer. \emph{Object-Oriented Program Construction}, Second
Edition, Prentice Hall, 1997.
\item[{[}Mossenbock 1995{]}:]
Hanspeter Mossenbock. \emph{Object-Oriented Programming in Oberon-2},
Springer-Verlag, 1995.
\item[{[}Thomas 1995{]}:]
Pete Thomas and Ray Weedom. \emph{Object-Oriented Programming in
Eiffel}, Addison-Wesley, 1995.
\end{description}

\hypertarget{terms-and-concepts}{%
\subsection{Terms and Concepts}\label{terms-and-concepts}}

TODO

\end{document}
