% Options for packages loaded elsewhere
\PassOptionsToPackage{unicode}{hyperref}
\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} % provide euro and other symbols
\else % if luatex or xetex
  \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 Abstract Data Types in Scala},
  pdfauthor={H. Conrad Cunningham},
  hidelinks,
  pdfcreator={LaTeX via pandoc}}
\urlstyle{same} % disable monospaced 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}}}}
\usepackage{graphicx,grffile}
\makeatletter
\def\maxwidth{\ifdim\Gin@nat@width>\linewidth\linewidth\else\Gin@nat@width\fi}
\def\maxheight{\ifdim\Gin@nat@height>\textheight\textheight\else\Gin@nat@height\fi}
\makeatother
% Scale images if necessary, so that they will not overflow the page
% margins by default, and it is still possible to overwrite the defaults
% using explicit options in \includegraphics[width, height, ...]{}
\setkeys{Gin}{width=\maxwidth,height=\maxheight,keepaspectratio}
% Set default figure placement to htbp
\makeatletter
\def\fps@figure{htbp}
\makeatother
\setlength{\emergencystretch}{3em} % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{-\maxdimen} % remove section numbering
\usepackage{caption}
\DeclareCaptionLabelFormat{nolabel}{}
\captionsetup{labelformat=nolabel}
\ifxetex
  % Load polyglossia as late as possible: uses bidi with RTL langages (e.g. Hebrew, Arabic)
  \usepackage{polyglossia}
  \setmainlanguage[]{english}
\else
  \usepackage[shorthands=off,main=english]{babel}
\fi

\title{CSci 555: Functional Programming\\
Abstract Data Types in Scala}
\author{\textbf{H. Conrad Cunningham}}
\date{\textbf{7 April 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 textbook requires a
browser that supports the display of MathML. A good choice as of April
2019 is a recent version of Firefox from Mozilla.

TODO: These Scala-based notes are not as consistent and fluent as they
should be. Revise them further.

\newpage

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

\hypertarget{introduction}{%
\subsection{Introduction}\label{introduction}}

These notes examine how to specify, design, and implement abstract data
types in Scala.

The goals of these notes are to:

\begin{itemize}
\item
  review the key concepts of modular design and programming
  (e.g.~modules, interfaces, information hiding, and contracts)
\item
  explore how to specify abstract data types using a constructive
  approach based on an abstract model of the data type
\item
  illustrate how to use Scala features (e.g traits and classes) to
  define appropriate interfaces and implement information-hiding modules
\item
  examine the design and implementation of a nontrivial abstract data
  type (i.e.~a doubly labelled directed graph)
\end{itemize}

The concepts and terminology in this chapter are mostly general. They
are applicable to most any language. Here we look specifically at Scala.
(I have implemented basically the same data abstraction module in
Haskell and Elixir.)

\hypertarget{modular-design-and-programming}{%
\subsection{Modular Design and
Programming}\label{modular-design-and-programming}}

In the provocative 1986 essay ``No Silver Bullet---Essence and Accidents
in Software Engineering,'' software engineering pioneer Fred Brooks
asserts that ``building software will always be hard'' because software
systems are inherently \emph{complex}, must \emph{conform} to all sorts
of physical, human, and software interfaces, must \emph{change} as the
system requirements evolve, and are inherently \emph{invisible} entities
{[}Brooks 1986{]}.

A decade later Brooks again observes, ``The best way to attack the
essence of building software is not to build it at all'' {[}Brooks
1995{]}. That is, software engineers should reuse both software and,
more importantly, software designs.

What was true in the 1980s is still true today. Although software
development tools and practices have evolved, removing some of the
``accidental'' properties of software development, the essential
difficulties remain. Complexity continues to increase. The interfaces to
which software must conform continue to change quickly and increase in
number. The requirements on software continue to evolve, driven by
inexorable changes in the environment and increasing penetration of
computerized processes into new aspects of society. Globalization
generates new requirements, which arise from both new opportunities and
new competition.

We often develop software systems in multiperson teams. In many cases,
the teams are geographically distributed, perhaps even across national
boundaries. Communication among team members adds complexity to software
development.

How should we approach software development in this contemporary
context?

As a starting point, let us again look to a software engineering
pioneer: David Parnas. Parnas focuses on how to decompose a system into
modules to achieve robustness with respect to change and potential reuse
of software. He stresses the clarity of thought more than the
sophistication of languages and tools.

Although Parnas and his colleagues published their ideas on
\emph{modular specification} in the 1970s and 1980s {[}Parnas 1972,
1976, 1979, 1985; Britton 1981{]}, the ideas are as relevant today as
they were when first published.

\hypertarget{what-is-a-module}{%
\subsubsection{What is a module?}\label{what-is-a-module}}

Parnas defines a \emph{module} as ``a work assignment given to a
programmer or group of programmers'' {[}Parnas 1978{]}. This is a
\emph{software engineering} view of a module.

In a programming language, a ``module'' may also be a program unit
defined with a construct or convention. This is a \emph{programming
language} view of a module.

Ideally, a language's module features should support the software
engineering module methods.

\hypertarget{information-hiding-modules-and-secrets}{%
\subsubsection{Information-hiding modules and
secrets}\label{information-hiding-modules-and-secrets}}

According to Parnas, the goals of \emph{modular design} are to {[}Parnas
1972{]}:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  enable programmers to understand the system by focusing on one module
  at a time (i.e.~\emph{comprehensibility}).
\item
  shorten development time by minimizing required communication among
  groups (i.e.~\emph{independent development}).
\item
  make the software system flexible by limiting the number of modules
  affected by significant changes (i.e.~\emph{changeability}).
\end{enumerate}

Parnas advocates the use of a principle he called \emph{information
hiding} to guide decomposition of a system into appropriate modules
(i.e.~work assignments). He points out that the connections among the
modules should have as few information requirements as possible
{[}Parnas 1972{]}.

In the Parnas approach, an information-hiding module:

\begin{itemize}
\item
  forms a \emph{cohesive} unit of functionality \emph{separate} from
  other modules
\item
  \emph{hides} a design decision---its \emph{secret}---from other
  modules
\item
  \emph{encapsulates} an aspect of system likely to change (its secret)
\end{itemize}

Aspects likely to change independently of each other should become
secrets of separate modules. Aspects unlikely to change can become
interactions (connections) among modules.

This approach supports the goal of changeability (goal 2). When care is
taken to design the modules as clean abstractions with well-defined and
documented interfaces, the approach also supports the goals of
independent development (goal 1) and comprehensibility (goal 3).

Information hiding has been absorbed into the dogma of contemporary
object-oriented programming. However, information hiding is often
oversimplified as merely hiding the data and their representations
{[}Weiss 2001{]}.

The secret of a well-designed module may be much more than that. It may
include such knowledge as a specific functional requirement stated in
the requirements document, the processing algorithm used, the nature of
external devices accessed, or even the presence or absence of other
modules or programs in the system {[}Parnas 1972, 1979, 1985{]}. These
are important aspects that may change as the system evolves.

\hypertarget{contracts-preconditions-and-postconditions}{%
\subsubsection{Contracts: Preconditions and
postconditions}\label{contracts-preconditions-and-postconditions}}

Let's review the concepts of precondition and postcondition, which
introduced in the notes on \emph{Recursion Styles, Correctness, and
Efficiency (Scala Version)} {[}Cunningham 2019b{]}.

The \emph{precondition} of a function is what the caller (i.e.~the
client of the function) must ensure holds when calling the function. A
precondition may specify the valid combinations of values of the
arguments. It may also record any constraints on any ``global'' state
that the function accesses or modifies.

If the precondition holds, the supplier (i.e.~developer) of the function
must ensure that the function terminates with the \emph{postcondition}
satisfied. That is, the function returns the required values and/or
alters the ``global'' state in the required manner.

We sometimes call the set of preconditions and postconditions for a
function the \emph{contract} for that function. These concepts underlie
Meyer's \emph{design by contract} approach to software development
{[}Meyer 1997{]}.

\hypertarget{interfaces}{%
\subsubsection{Interfaces}\label{interfaces}}

It is important for information-hiding modules to have well-defined and
stable interfaces.

According to Britton, Parker, and Parnas, an \emph{interface} is a ``set
of assumptions \ldots{} each programmer needs to make about the other
program \ldots{} to demonstrate the correctness of his own program''
{[}Britton 1981{]}.

A module's interface includes the type signatures (i.e.~names,
arguments, and return values), preconditions, and postconditions of all
public operations (e.g.~functions).

As we see later, the interface also includes the \emph{invariant}
properties of the data values and structures manipulated by the module
and the definitions of any new data types exported by the module. An
invariant must be part of the precondition of public operations except
operations that construct elements of the data type (i.e.~constructors).
It must also be part of the postcondition of public operations except
operations that destroy elements of the data type (i.e.~destructors).

In Scala, we often use a \VERB|\KeywordTok{trait}|, a
\VERB|\KeywordTok{class}|, or an \VERB|\KeywordTok{object}| to implement
the module.

\hypertarget{abstract-interfaces}{%
\subsubsection{Abstract interfaces}\label{abstract-interfaces}}

An \emph{abstract interface} is an interface that does not change when
one module implementation is substituted for another {[}Britton 1981;
Parnas 1978{]}. It concentrates on module's essential aspects and
obscures incidental aspects that vary among implementations.

Information-hiding modules and abstract interfaces enable us to design,
build, and test software systems with multiple versions. The
information-hiding approach seeks to identify aspects of a software
design that might change from one version to another and to hide them
within independent modules behind well-defined abstract interfaces.

We can reuse the software design across several similar systems. We can
reuse an existing module implementation when appropriate. When we need a
new implementation, we can create one by following the specification of
the module's abstract interface.

In Scala, we often use a \VERB|\KeywordTok{trait}| (or an
\VERB|\KeywordTok{abstract} \KeywordTok{class}|) to specify an abstract
interface in concrete form so that we can use it for several
``modules''.

\hypertarget{client-supplier-relationship}{%
\subsubsection{Client-supplier
relationship}\label{client-supplier-relationship}}

The design and implementation of information-hiding modules must be
approached from two points of view simultaneously {[}Meyer 1997{]}:

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

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

TODO: Provide a better drawing below.

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

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

The supplier's concerns include:

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

The clients' concerns include:

\begin{itemize}
\item
  accomplishing their own tasks
\item
  using the supplier module 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 a module 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-interfaces}{%
\subsubsection{Design criteria for
interfaces}\label{design-criteria-for-interfaces}}

What else should we consider in designing a good interface for an
information-hiding module (e.g.~a Scala \VERB|\KeywordTok{trait}|,
\VERB|\KeywordTok{class}|, or \VERB|\KeywordTok{object}|)?

In designing an interface for a module, we should also consider the
following criteria. Of course, some of these criteria conflict with one
another; a designer must carefully balance the criteria to achieve a
good interface design.

Note: These are general principles; they are not limited to Scala or
functional programming. In object-oriented languages, these criteria
apply to class interfaces, whether the instances are immutable or
mutable.

\begin{itemize}
\item
  \textbf{Cohesion:} All operations must logically fit together to
  support a single, coherent purpose. The module should describe a
  single abstraction.
\item
  \textbf{Simplicity:} Avoid needless features. The smaller the
  interface the easier it is to use the module.
\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 module.
\item
  \textbf{Consistency:} Provide a set of operations that are internally
  consistent in

  \begin{itemize}
  \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.

  The operations should be consistent with good practices for the
  specific language being used.
\item
  \textbf{Reusability:} Do not customize modules 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 module so that it remains stable even if the
  implementation of the module changes. (That is, it should be an
  abstract interface for an information-hiding module as we discussed
  above.)
\item
  \textbf{Convenience:} Where appropriate, provide additional operations
  (e.g., beyond the complete primitive set) for the convenience of users
  of the module. Add convenience operations only for frequently used
  combinations after careful study.
\end{itemize}

We must trade off conflicts among the criteria. For example, we must
balance:

\begin{itemize}
\item
  completeness versus simplicity
\item
  reusability versus simplicity
\item
  convenience versus consistency, simplicity, no redundancy, and
  atomicity
\end{itemize}

We must also balance these design criteria against efficiency and
functionality.

\hypertarget{terminology}{%
\subsection{Terminology}\label{terminology}}

The remainder of these notes use the term \emph{abstract data type} to
refer to a data abstraction. A data abstraction ``module'' defines and
exports a user-defined type and a set of operations on that type. The
type is abstract in the sense that its concrete representation is
hidden; only the module's operations may manipulate the representation
directly.

For convenience, these notes sometimes use acronym \emph{ADT} to refer
to an abstract data type. The term abstract data type or acronym ADT
should not be confused with algebraic data type, which we have discussed
previously. We specify an algebraic data type with rules on how to
compose and decompose them---primarily with syntax. We specify an
abstract data type with rules about how the operations behave in
relation to one another---primarily with semantics.

\hypertarget{case-study-doubly-labelled-digraph}{%
\subsection{Case Study: Doubly Labelled
Digraph}\label{case-study-doubly-labelled-digraph}}

In these notes, we develop a family of \emph{doubly labelled digraph}
data structures.

As a \emph{graph}, the data structure consists of a finite set of
\emph{vertices (nodes)} and a set of \emph{edges}. Each edge connects
two vertices.

Note: Some writers require that the set of vertices be nonempty, but
here we prefer to allow an empty graph to have no vertices. (But the
question remains whether such a graph with no vertices is pointless
concept.)

As a \emph{directed graph} (or \emph{digraph}), each pair of vertices
has at most one edge connecting them; the edge has a direction from one
of the edges to the other.

As a \emph{doubly labelled} graph, each vertex and each edge has some
user-defined data (i.e.~labels) attached.

These notes draw on the discussion of digraphs and their specification
in Chapters 1 and 10 of the Dale and Walker book \emph{Abstract Data
Types} {[}Dale 1996{]}.

\hypertarget{use-case}{%
\subsection{Use Case}\label{use-case}}

For what purpose can we use a doubly labelled digraph data structure?

One concrete use case is to represent the game world in an
implementation of an adventure game.

For example, in the Wizard's Adventure Game from Chapter 5 of reference
{[}Barski 2011{]}, the game's rooms become vertices, passages between
rooms become edges, and descriptions associated with rooms or passages
become labels on the associated vertex or edge (as shown in Figure 1).

\begin{figure}
\centering
\includegraphics{fig_05_01.png}
\caption{\textbf{Figure 1: Labelled Digraph for Wizard's Adventure
Game}}
\end{figure}

Aside: By using a digraph to model the game world, we disallow multiple
passages directly from one room to another. By changing the graph to a
\emph{multigraph}, we can allow multiple directed edges from one vertex
to another.

The Adventure game must create and populate the game world initially,
but it does not typically modify the game world during play. It
maintains the game state (e.g.~player location) separately from the game
world. A player moves from room to room during play; the labelled
digraph gives the static structure and descriptions of the game world.

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

How can we define an abstract data type?

The behavior of an ADT is defined by a set of operations that can be
applied to an \emph{instance} of the ADT (e.g.~a Scala object).

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.

\hypertarget{specification}{%
\subsubsection{Specification}\label{specification}}

To specify an ADT, we need to give:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\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}

\hypertarget{operations}{%
\subsubsection{Operations}\label{operations}}

We categorize an ADT's operations into 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 normally list the operations in that order.

If we use immutable data structures, then 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 take an applicative (or
functional or referentially transparent) approach to ADT specifications.

If we use mutable data structures, then a mutator can change the state
of an instance in place. That may be more efficient, but it tends to be
less safe. It also tends to make concurrent use of an abstract data type
more problematic.

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

\hypertarget{approaches-to-semantics}{%
\subsubsection{Approaches to semantics}\label{approaches-to-semantics}}

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.

In these notes, we use the constructive approach. We use
contracts---preconditions, postconditions, and invariants---to specify
the semantics of the operations.

\hypertarget{invariants}{%
\subsubsection{Invariants}\label{invariants}}

A module that implements an ADT must ensure that the objects it creates
and manipulates maintain their integrity---always have a valid structure
and state.

These properties are \emph{invariant} for the ADT operations. An
invariant for the data abstraction can help us design and implement such
objects.

\begin{description}
\item[\emph{Invariant}:]
A logical assertion that must always be true for every ``object''
created by the public constructors and manipulated only by the public
operations of the data abstraction.
\end{description}

An invariant is a precondition of all operations except constructors and
a postcondition of all operations except destructors.

Often, we separate an invariant into two parts.

\begin{description}
\item[\emph{Interface invariant}:]
An invariant stated in terms of the public features and abstract
properties of the ``object''.
\item[\emph{Implementation (representation) invariant}:]
A detailed invariant giving the required relationships among the
internal features of the implementation of an ``object''
\end{description}

An interface invariant is a key aspect of the \emph{abstract interface}
of an ADT module. It is useful to the users of the module, as well to
the developers.

It is important to note that an invariant is not required to hold:

\begin{itemize}
\item
  for private operations (e.g.~functions, procedures, or methods) within
  an implementation of an ADT
\item
  at any point within the implementation of an operation except the
  beginning and the end
\end{itemize}

\hypertarget{specification-of-labelled-digraph-adt}{%
\subsection{Specification of Labelled Digraph
ADT}\label{specification-of-labelled-digraph-adt}}

Now let's look at a constructive specification of the doubly labelled
digraph.

First, we specify the ADT as an implementation-independent abstraction.
The \emph{secret} of the ADT module is the data structure used
internally to implement the doubly labelled digraph.

Then, we examine two implementations of the abstraction:

\begin{itemize}
\item
  using Scala lists to represent the vertex and edge sets
\item
  using a Scala \VERB|\NormalTok{Map}| to map a vertex to the set of
  outgoing edges from that vertex
\end{itemize}

Before we specify the ADT, let's define the mathematical notation we
use. We choose notation that can readily be used in comments in program.

\hypertarget{notation}{%
\subsubsection{Notation}\label{notation}}

We use the following notation and terminology to describe the abstract
data type's model and its semantics. (In this case study, we use
notation that can be easily included as textual comments in source code
rather than using special mathematical and logical symbols.)

TODO: Perhaps either expand this to be more general or contract it to
just the concepts needed for these notes. Perhaps change these notes to
use standard mathematical symbols.

\begin{itemize}
\item
  \texttt{(ForAll\ x,\ y\ ::\ p(x,y))} is true if and only if predicate
  \texttt{p(x,y)} is true for all values of \texttt{x} and \texttt{y}.
\item
  \texttt{(Exists\ x,\ y\ ::\ p(x,y))} is true if and only if there is
  at least one pair of values \texttt{x} and \texttt{y} for which
  \texttt{p(x,y)} is true.
\item
  \texttt{(\#\ x,\ y\ ::\ p(x,y))} yields a count of pairs
  \texttt{(x,y)} for which \texttt{p(x,y)} is true.
\item
  \texttt{\textless{}=\textgreater{}} denotes logical equivalence.
  \texttt{p\ \textless{}=\textgreater{}\ q} is true if and only if the
  logical (Boolean) values \texttt{p} and \texttt{q} are equal
  (i.e.~both true or both false).
\item
  \texttt{x\ IN\ C} is true if and only if value \texttt{x} is member of
  a collection \texttt{C} (such as a set, bag, or sequence). Similarly,
  \texttt{x\ NOT\_IN\ C} denotes the negation of \texttt{x\ IN\ C}.
\item
  A type consists of a set of values and a set of operations. We
  sometimes say a value is \texttt{IN} a type to mean the value is
  \texttt{IN} the set associated with the type.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ UNION\ D} denotes set
  union, that is, a set that includes all the element of both \texttt{C}
  and \texttt{D}.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ INTERSECT\ D} denotes
  set intersection, that is, a set that includes all elements that are
  both in \texttt{C} and in \texttt{D}.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ -\ D} denotes set
  difference, that is, the set \texttt{C} with all elements of set
  \texttt{D} removed.
\item
  For sets \texttt{C} and \texttt{D}, \texttt{C\ SUBSET\_OF\ D} denotes
  that \texttt{C} is subset of \texttt{D}, that is, all the elements of
  \texttt{C} also occur in \texttt{D}.
\item
  A \emph{Cartesian product} of two sets \texttt{C} and \texttt{D} is
  the set of all \emph{ordered pairs} \texttt{(x,y)} where
  \texttt{x\ IN\ C} and \texttt{y\ IN\ D}.
\item
  A tuple such as \texttt{(x,*)} appearing in a collection such as
  \texttt{\{\ (x,*)\ \}} denotes element \texttt{x} grouped with all
  possible values of the second component. Note: We could also write
  \texttt{\{\ (x,*)\ \}} using a quantification as:

\begin{verbatim}
    { (x,c) :: c IN some_domain }
\end{verbatim}
\item
  A \emph{relation} on sets \texttt{C} and \texttt{D} is a subset of the
  Cartesian product of \texttt{C} and \texttt{D}. That is, a set of
  tuples.
\item
  A \emph{function} on sets \texttt{C} and \texttt{D} is a special case
  of a relation on \texttt{C} and \texttt{D} where each value from
  \texttt{C} occurs in at most one tuple in the relation.
\item
  A \emph{total function} is defined for all elements of its domain. A
  \emph{partial function} is defined for a subset of the elements of its
  domain.
\end{itemize}

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

The abstract data type being defined is named
\VERB|\NormalTok{Digraph}|.

We specify that this abstract data type be represented by a Scala
generic type

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{    Digraph[VertexType,VertexLabelType,EdgeLabelType]}
\end{Highlighting}
\end{Shaded}

which has three type parameters (i.e.~sets):

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  Type (or set) \VERB|\NormalTok{VertexType}| denotes the possible
  vertices (i.e.~vertex identifiers) in the \VERB|\NormalTok{Digraph}|.
\item
  Type (or set) \VERB|\NormalTok{VertexLabelType}| denotes the possible
  labels on vertices in the \VERB|\NormalTok{Digraph}|.
\item
  Type (or set) \VERB|\NormalTok{EdgeLabelType}| denotes the possible
  labels on edges in the \VERB|\NormalTok{Digraph}|.
\end{enumerate}

Given this ADT defines a digraph, edges can be identified by ordered
pairs (tuples) of vertices.

Values of the above types, in particular the labels, may have several
components.

Values the above types, in particular the labels, may have several
components.

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

We define the following operations on the Labelled Digraph ADT. We
specify these as methods on a Scala trait \VERB|\NormalTok{Digraph}|.
The methods have an implicit argument \VERB|\KeywordTok{this}|, which is
an object from a concrete class that extends the trait (i.e.~the
receiver or target object for the method).

For conciseness, we use short generic parameter names
\VERB|\NormalTok{A}|, \VERB|\NormalTok{B}|, and \VERB|\NormalTok{C}| for
\VERB|\NormalTok{VertexType}|, \VERB|\NormalTok{VertexLabelType}|, and
\VERB|\NormalTok{EdgeLabelType}|, respectively.

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{trait}\NormalTok{ Digraph[A,B,C] \{ }\CommentTok{// A = VertexType, B = VertexLabelType, }
                           \CommentTok{// C = EdgeLabelType}
\end{Highlighting}
\end{Shaded}

TODO: Probably should use better generic parameters than A, B, C.

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

Given the primary use case described above, we require a
\emph{zero-parameter constructor} that creates an empty graph. A
concrete class that extends the trait may include other constructors.

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

Given the primary use case described above, we specify mutators to add a
new vertex (\VERB|\NormalTok{addVertex}|) and add a new edge between
existing vertices (\texttt{addEdge}\{.scala).

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{addVertex}\NormalTok{(nv:A, nl:B): Digraph[A,B,C]}
    \KeywordTok{def} \FunctionTok{addEdge}\NormalTok{(v1:A, v2:A, nl:C): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

We also specify mutators to remove a vertex
(\VERB|\NormalTok{removeVertex}|), remove an edge
(\VERB|\NormalTok{removeEdge}|), update the labels on a vertex
(\texttt{updateVertex}, and update the label on an edge
(\VERB|\NormalTok{updateEdge}|). (Note: In the identified use case,
these are likely used less often than the mutators that add new vertices
and edges. But we include them for completeness.)

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{removeVertex}\NormalTok{(ov:A): Digraph[A,B,C]}
    \KeywordTok{def} \FunctionTok{removeEdge}\NormalTok{(v1:A, v2:A): Digraph[A,B,C]}
    \KeywordTok{def} \FunctionTok{updateVertex}\NormalTok{(ov:A, nl:B): Digraph[A,B,C]}
    \KeywordTok{def} \FunctionTok{updateEdge}\NormalTok{(v1:A, v2:A, nl:C): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

Note: To remove a vertex requires us to remove any edges attached to
that vertex.

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

We specify query functions to check whether the labelled digraph is
empty (\VERB|\NormalTok{isEmpty}|), has a given vertex
(\VERB|\NormalTok{hasVertex}|), and has an edge between two vertices
(\VERB|\NormalTok{hasEdge}|).

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def}\NormalTok{ isEmpty: Boolean}
    \KeywordTok{def} \FunctionTok{hasVertex}\NormalTok{(v:A): Boolean }
    \KeywordTok{def} \FunctionTok{hasEdge}\NormalTok{(v1:A, v2:A): Boolean}
\end{Highlighting}
\end{Shaded}

We specify accessors to retrieve the label associated with a given
vertex (\VERB|\NormalTok{getVertex}|) and with a given edge
(\VERB|\NormalTok{getEdge}|).

\begin{verbatim}
    def getVertexLabel(ov:A): B
    def getEdgeLabel(v1:A, v2:A): C
\end{verbatim}

Given the identified use case, we also specify accessors to return a
list of all vertices in the graph (\VERB|\NormalTok{allVertices}|) and
of the pairing of all vertices with their labels
(\VERB|\NormalTok{allVerticesLabels}|).

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def}\NormalTok{ allVertices: List[A]}
    \KeywordTok{def}\NormalTok{ allVerticesLabels: List[(A,B)]}
\end{Highlighting}
\end{Shaded}

Similarly, we specify accessors to return a list of all outgoing edges
from a given vertex (\VERB|\NormalTok{fromEdges}|) and of the pairing of
all outgoing edges with their edge labels
(\VERB|\NormalTok{fromEdgesLabels}|). Here we identify outgoing edge by
the ``to'' vertex for that edge.

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{fromEdges}\NormalTok{(v1:A): List[A]}
    \KeywordTok{def} \FunctionTok{fromEdgesLabels}\NormalTok{(v1:A): List[(A,C)]}
\end{Highlighting}
\end{Shaded}

Question: What other operations might be useful?

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

We do not specify any separate destructors. We rely on the garbage
collection of the objects. (In some cases, concrete classes that
implement abstract data types may need to implement explicit destructors
to deallocate resources such as open files, network connections, etc.)

\hypertarget{semantics}{%
\subsubsection{Semantics}\label{semantics}}

We \emph{model} the state of the instance of the Labelled Digraph ADT
with an abstract value \texttt{G} such that \texttt{G\ =\ (V,E,VL,EL)}
with \texttt{G}'s components satisfying the following \emph{Labelled
Digraph Properties}.

\begin{itemize}
\item
  \texttt{V} is a finite subset of values from the set
  \VERB|\NormalTok{VertexType}|. \texttt{V} denotes the vertices (or
  nodes) of the digraph.
\item
  Any two elements of \texttt{V} can be compared for \emph{equality}.

  Some implementations of the \VERB|\NormalTok{Digraph}| may further
  require that the set \texttt{V} be:

  \begin{itemize}
  \item
    totally ordered---supporting \VERB|\NormalTok{<}| and the other
    relational operators
  \item
    hashable
  \end{itemize}
\item
  \texttt{E} is a binary relation on the set \texttt{V}. A pair
  \texttt{(v1,v2)\ IN\ E} denotes that there is a directed edge from
  \texttt{v1} to \texttt{v2} in the digraph.

  Note that this model allows at most one (directed) edge from a vertex
  \texttt{v1} to vertex \texttt{v2}. It allows a directed edge from a
  vertex to itself.

  Also, because vertices can be compared for equality, any two edges can
  also be compared for equality.
\item
  \texttt{VL} is a total function from set \texttt{V} to the set
  \VERB|\NormalTok{VertexLabelType}|.
\item
  \texttt{EL} is a total function from set \texttt{E} to the set
  \VERB|\NormalTok{EdgeLabelType}|.
\end{itemize}

\hypertarget{interface-invariant}{%
\paragraph{Interface invariant}\label{interface-invariant}}

We define the following interface invariant for the Labelled Digraph
ADT:

\begin{quote}
\emph{Any valid labelled digraph instance \texttt{G}, appearing in
either the arguments or return value of a public ADT operation, must
satisfy the Labelled Digraph Properties.}
\end{quote}

\hypertarget{constructive-semantics}{%
\paragraph{Constructive semantics}\label{constructive-semantics}}

We specify the various ADT operations below using their type signatures,
preconditions, and postconditions. Along with the interface invariant,
these comprise the (implementation-independent) specification of the ADT
(i.e.~its abstract interface).

In these assertions, for a digraph object \VERB|\KeywordTok{this}| that
satisfies the invariants, \texttt{G(this)} denotes its abstract model
\texttt{(V,E,VL,EL)} as described above. The value \texttt{Result}
denotes the return value of method.

Given this family of implementations uses immutable graph objects, every
operation, both accessor and mutator, has a postcondition conjunct

\begin{verbatim}
    G(this) = G(this')
\end{verbatim}

where \VERB|\KeywordTok{this}| denotes the receiver object before the
operation and \VERB|\NormalTok{this'}| denotes the receiver object after
the operation.

For an implementation allowing mutable graph objects, this requirement
may be relaxed for some mutators. However, it should still hold for all
accessors.

\begin{itemize}
\item
  A parameterless constructor creates and returns a new empty instance
  of the graph ADT.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
true
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == ({},{},{},{})
\end{verbatim}

    For a Scala class constructor, the \texttt{Result} is a new instance
    of the data type created by the constructor. Thus the postcondition
    is equivalent to
    \texttt{G(this\textquotesingle{})\ ==\ (\{\},\{\},\{\},\{\})}.
  \end{itemize}
\item
  Mutator method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{addVertex}\NormalTok{(nv:A, nl:B): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

  inserts vertex \VERB|\NormalTok{nv}| with label \VERB|\NormalTok{nl}|
  into graph \VERB|\KeywordTok{this}| and returns the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL) && nv NOT_IN V
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V UNION {nv}, E, VL UNION {(nv,nl)}, EL)
\end{verbatim}
  \end{itemize}

  Note: The set operation \texttt{VL\ UNION\ \{(nv,nl)\}} redefines the
  function (i.e.~a type of relation) \texttt{VL} so that vertex
  \texttt{nv} now maps to vertex label \texttt{nl} (where there was no
  mapping beforehand).

  If the precondition is true, then the method must terminate with the
  postcondition being true. The specification does not say what must
  occur if the precondition is false.

  Consider the following questions:

  \begin{itemize}
  \item
    Can we remove the \texttt{nv\ NOT\_IN\ V} conjunct in the
    precondition? (That is, can we \emph{weaken} the precondition in
    this way?)
  \item
    If so, what are ways we can modify the postcondition to handle the
    new input states? (That is, how do we \emph{strengthen} the
    postcondition by adding new conjuncts for the new input states?)
  \item
    Would it be appropriate to redefine the operation's signature and
    semantics to return an object of type
    \VERB|\NormalTok{Option[Diagraph[A,B,C]]}|? of some
    \VERB|\NormalTok{Either}| type? What are advantages and
    disadvantages of this kind of change?
  \end{itemize}
\item
  Mutator method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{removeVertex}\NormalTok{(ov:A): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

  deletes vertex \VERB|\NormalTok{ov}| from graph
  \VERB|\KeywordTok{this}| and returns the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) =  (V,E,VL,EL) && ov IN V
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V', E', VL', EL') 
    where V'  = V  - {ov}
          E'  = E  - {(ov,*),(*,ov)}
          VL' = VL - {(ov,*)}
          EL' = EL - {((ov,*),*),((*,ov),*)}
\end{verbatim}

    This operation also removes all edges attached to the vertex
    removed.

    Question: Can we remove the \texttt{ov\ IN\ V} conjunct in the
    precondition? If so, what are ways we can modify the postcondition
    to handle the new input states?
  \end{itemize}
\item
  Mutator method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{updateVertex}\NormalTok{(ov:A, nl:B): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

  changes the label on vertex \VERB|\NormalTok{ov}| in graph
  \VERB|\KeywordTok{this}| to be \VERB|\NormalTok{nl}| and returns the
  resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) =  (V,E,VL,EL) && ov IN V 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V - {ov}, E, VL', EL) 
    where VL' = (VL - {(ov,VL(ov))}) UNION {(ov,nl)}
\end{verbatim}

    Question: Can we remove the \texttt{ov\ IN\ V} conjunct in the
    precondition? If so, what are ways we can modify the postcondition
    to handle the new input states?
  \end{itemize}
\item
  Mutator method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{addEdge}\NormalTok{(v1:A, v2:A, nl:C): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

  inserts an edge from vertex \VERB|\NormalTok{v1}| to vertex
  \VERB|\NormalTok{v2}| with label \VERB|\NormalTok{nl}| in graph
  \VERB|\KeywordTok{this}| and returns the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL) && v1 IN V && v2 IN V && 
(v1,v2) NOT_IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V, E', VL, EL') 
    where E'  = E  UNION {(v1,v2)}
          EL' = EL UNION {((v1,v2),nl)}
\end{verbatim}
  \end{itemize}

  Question: Can we weaken the precondition?
\item
  Mutator method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{removeEdge}\NormalTok{(v1:A, v2:A): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

  deletes the edge from vertex \VERB|\NormalTok{v1}| to vertex
  \VERB|\NormalTok{v2}| from graph \VERB|\KeywordTok{this}| and returns
  the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) =  (V,E,VL,EL) && (v1,v2) IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V, E - {(v1,v2)}, VL, EL - { ((v1,v2),*) }
\end{verbatim}
  \end{itemize}

  Question: Can we weaken the precondition?
\item
  Mutator method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{updateEdge}\NormalTok{(v1:A, v2:A, nl:C): Digraph[A,B,C]}
\end{Highlighting}
\end{Shaded}

  changes the label on the edge from vertex \VERB|\NormalTok{v1}| to
  vertex \VERB|\NormalTok{v2}| in graph \VERB|\KeywordTok{this}| to have
  label \VERB|\NormalTok{nl}| and then returns the resulting graph.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL) && (v1,v2) IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == (V, E, VL, EL') 
    where EL' == (EL - {((v1,v2),*)}) UNION {((v2,v2),nl) 
\end{verbatim}
  \end{itemize}

  Question: Can we weaken the precondition?
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def}\NormalTok{ isEmpty: Boolean}
\end{Highlighting}
\end{Shaded}

  returns \VERB|\KeywordTok{true}| if and only if graph
  \VERB|\KeywordTok{this}| is empty.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == (V == {} && E == {})
\end{verbatim}
  \end{itemize}
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{hasVertex}\NormalTok{(ov:A): Boolean}
\end{Highlighting}
\end{Shaded}

  returns \VERB|\KeywordTok{true}| if and only if \VERB|\NormalTok{ov}|
  is a vertex of graph \VERB|\KeywordTok{this}|.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
G(Result) == ov IN V 
\end{verbatim}
  \end{itemize}
\item
  Accessor method

\begin{verbatim}
    def hasEdge(v1:A, v2:A): Boolean
\end{verbatim}

  returns \VERB|\KeywordTok{true}| if and only if there is an edge from
  a vertex \VERB|\NormalTok{v1}| to a vertex \VERB|\NormalTok{v2}| in
  graph \VERB|\KeywordTok{this}|.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == (v1,v2) IN E 
\end{verbatim}
  \end{itemize}
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{getVertex}\NormalTok{(ov:A): B}
\end{Highlighting}
\end{Shaded}

  returns the label from vertex \VERB|\NormalTok{ov}| in graph
  \VERB|\KeywordTok{this}|

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL) && ov IN V 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == VL(ov) 
\end{verbatim}
  \end{itemize}

  Question: Can we weaken the precondition?
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{getEdge}\NormalTok{(v1:A, v2:A): C}
\end{Highlighting}
\end{Shaded}

  returns the label on the edge from vertex \VERB|\NormalTok{v1}| to
  vertex \VERB|\NormalTok{v2}| in graph \VERB|\KeywordTok{this}|.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(g) = (V,E,VL,EL) && (v1,v2) IN E
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Result == EL((v1,v2))
\end{verbatim}
  \end{itemize}

  Question: Can we weaken the precondition?
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def}\NormalTok{ allVertices: List[A]}
\end{Highlighting}
\end{Shaded}

  returns a List of all the vertices in graph \VERB|\KeywordTok{this}|.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL) 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll ov:: ov IN Result <=> ov IN V) && 
length(Result) == size(V) 
\end{verbatim}
  \end{itemize}

  This returns the set \texttt{V} as a Scala \VERB|\NormalTok{List}|
  without duplicates. The order of the elements in the list is not
  specified. (Remember that the set \VERB|\NormalTok{VertexType}| is not
  necessarily partially or totally ordered, but it does support equality
  comparisons)
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{fromEdges}\NormalTok{(v1:A): List(A)}
\end{Highlighting}
\end{Shaded}

  returns a sequence of all vertices \VERB|\NormalTok{v2}| such that
  there is an edge from vertex \VERB|\NormalTok{v1}| to vertex
  \VERB|\NormalTok{v2}| in graph \VERB|\KeywordTok{this}|.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL) && v1 IN V 
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll v2:: v2 IN Result <=> (v1,v2) IN E) &&
length(Result) == (# v2 :: (v1,v2) IN E) 
\end{verbatim}
  \end{itemize}

  Question: Can we remove the precondition conjunct \texttt{v1\ IN\ V}?

  Method call \VERB|\FunctionTok{fromEdges}\NormalTok{(v1)}| probably
  should return \VERB|\NormalTok{List()}| when \VERB|\NormalTok{v1}|
  does not appear in \VERB|\KeywordTok{this}|. This will make it can
  work well with the Wizard's Adventure game. To do so, we can redefine
  the precondition and postcondition to specify appropriate behavior.

  \begin{itemize}
  \item
    Revised Precondition (weaker):

\begin{verbatim}
G(this) = (V,E,VL,EL)
\end{verbatim}
  \item
    Revised Postcondition (stronger):

\begin{verbatim}
(v1 NOT_IN V => Result == List()) 
&&
(v1 IN V =>
    (ForAll v2:: v2 IN Result <=> (v1,v2) IN E) &&
    length(Result) == (# v2 :: (v1,v2) IN E) )
\end{verbatim}
  \end{itemize}
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def}\NormalTok{ allVerticesLabels: List[(A,B)]}
\end{Highlighting}
\end{Shaded}

  returns a sequence of all pairs \VERB|\NormalTok{(v,l)}| such that
  \VERB|\NormalTok{v}| is a vertex and \VERB|\NormalTok{l}| is it's
  label in graph \VERB|\KeywordTok{this}|.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll v, l:: (v,l) IN Result <=> (v,l) IN VL) && 
length(Result) == size(VL) 
\end{verbatim}
  \end{itemize}
\item
  Accessor method

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \FunctionTok{fromEdgesLabels}\NormalTok{(v1:A): List[(A,C)]}
\end{Highlighting}
\end{Shaded}

  returns a List of all pairs \VERB|\NormalTok{(v2,l)}| such that there
  is an edge \VERB|\NormalTok{(v1,v2)}| labelled with
  \VERB|\NormalTok{l}| in graph \VERB|\KeywordTok{this}|.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
G(this) = (V,E,VL,EL) && v1 IN V
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll v2, l :: (v2,l) IN Result <=> ((v1,v2),l) IN EL) 
&& length(Result) == (# v2 :: (v1,v2 ) IN E) 
\end{verbatim}
  \end{itemize}

  Question: Can we remove the precondition conjunct \texttt{v1\ IN\ V}?

  Method call \VERB|\FunctionTok{fromEdgesLabels}\NormalTok{(v1)}|
  probably should return \VERB|\NormalTok{List()}| when
  \VERB|\NormalTok{v1}| does not appear in \VERB|\KeywordTok{this}|.
  This will make it can work well with the Wizard's Adventure game. To
  do so, we can redefine the precondition and postcondition to specify
  appropriate behavior.

  \begin{itemize}
  \item
    Revised Precondition (weaker):

\begin{verbatim}
G(this) = (V,E,VL,EL)
\end{verbatim}
  \item
    Revised Postcondition (stronger):

\begin{verbatim}
(v1 NOT_IN V => Result == List()) 
&&
(v1 IN V =>
  (ForAll v2, l :: (v2,l) IN Result <=> ((v1,v2),l) IN EL) 
  && length(Result) == (# v2 :: (v1,v2 ) IN E) )
\end{verbatim}
  \end{itemize}
\end{itemize}

\hypertarget{abstract-interface-in-scala}{%
\subsubsection{Abstract interface in
Scala}\label{abstract-interface-in-scala}}

We specify the abstract interface for the family of Scala
implementations of the \VERB|\NormalTok{Digraph}| ADT using a generic
Scala trait \VERB|\NormalTok{Digraph[A,B,C]}|, defined in file
\href{Digraph.scala}{\texttt{Digraph.scala}}.

The trait defines the interface to the mutator and accessor methods. The
construtor and destructor methods are left for the implementing class to
implement. We document the semantics as comments in the Scala source
code.

\hypertarget{list-implementation}{%
\subsection{List Implementation}\label{list-implementation}}

This section gives an implementation of the ADT that uses Scala lists to
represent the vertex and edge sets.

Conceptually, the approach taken here is a variation on the
\emph{adjacency matrix} representation of a graph. However, unlike the
typical presentation in an algorithms and data structures course, the
approach here does not restrict the set of vertices to be from a finite
range of integers.

\hypertarget{labelled-digraph-representation}{%
\subsubsection{Labelled digraph
representation}\label{labelled-digraph-representation}}

We represent the List implementation of the Labelled Digraph ADT as a a
Scala class \VERB|\NormalTok{DigraphList[A,B,C]}| that extends
\VERB|\NormalTok{Digraph[A,B,C]}|. (Remember that type variable
\VERB|\NormalTok{A}| is \VERB|\NormalTok{VertexType}|,
\VERB|\NormalTok{B}| is \VERB|\NormalTok{VertexLabelType}|, and
\VERB|\NormalTok{C}| is \VERB|\NormalTok{EdgeLabelType}|.)

We use the following \emph{primary constructor} for this Scala class.

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{class}\NormalTok{ DigraphList[A,B,C] }\KeywordTok{private}  \CommentTok{// private constructor}
\NormalTok{        (}\KeywordTok{private} \KeywordTok{val}\NormalTok{ vs: List[(A,B)], }
         \KeywordTok{private} \KeywordTok{val}\NormalTok{ es: List[(A,A,C)])}
        \KeywordTok{extends}\NormalTok{ Digraph[A,B,C] \{ ... \}}
\end{Highlighting}
\end{Shaded}

Above we use Scala features that we have not used before.

\begin{itemize}
\item
  We declare a Scala constructor parameter (i,e. object field) as
  \VERB|\KeywordTok{var}|, \VERB|\KeywordTok{val}|, or neither.

  \begin{itemize}
  \item
    \VERB|\KeywordTok{var}| means that the Scala compiler automatically
    generates a mutable instance variable with both public getter and
    setter methods.
  \item
    \VERB|\KeywordTok{val}| means that the Scala compiler automatically
    generates an immutable instance variable with a public getter
    method.
  \item
    Neither means that any variable that the Scala compiler generates
    will be immutable and will not have automatically generated public
    getter or setter methods. If the parameter is not used outside the
    initialization of the class, then no instance variable is generated.
  \end{itemize}
\item
  We can add the modifier \VERB|\KeywordTok{private}| to Scala
  constructor parameters: \VERB|\KeywordTok{private} \KeywordTok{var}|
  or \VERB|\KeywordTok{private} \KeywordTok{val}|. This means the
  compiler will not generate public getter and setter methods.
\item
  We can declare the primary constructor as \VERB|\KeywordTok{private}|.
  That means it can only be called from inside the class. (In such a
  case, we may need to have an auxiliary constructor that is public.)
\end{itemize}

Now let's consider how we use these fields to represent the abstract
data type.

In an instance \VERB|\FunctionTok{DigraphList}\NormalTok{(vs,es)}|:

\begin{itemize}
\item
  \VERB|\NormalTok{vs}| is a list of tuples \VERB|\NormalTok{(v,vl)}|
  where

  \begin{itemize}
  \tightlist
  \item
    \VERB|\NormalTok{v}| has type \VERB|\NormalTok{VertexType}|
    (i.e.~\VERB|\NormalTok{A}|) and represents a vertex of the digraph
  \item
    \VERB|\NormalTok{vl}| has type \VERB|\NormalTok{VertexLabelType}|
    (i.e.~\VERB|\NormalTok{B}|) and is the label associated with vertex
    \VERB|\NormalTok{v}|
  \item
    a vertex \VERB|\NormalTok{v}| occurs at most once in
    \VERB|\NormalTok{vs}| (i.e.~\VERB|\NormalTok{vs}| encodes a function
    from vertices to vertex labels)
  \end{itemize}

  Note: A list list \VERB|\NormalTok{vs}| is sometimes called an
  \emph{association list} because it associates a key
  (e.g.~\texttt{v}\{.scala{]}) with its value
  (e.g.~\VERB|\NormalTok{vl}|).
\item
  \VERB|\NormalTok{es}| is a list of tuples
  \VERB|\NormalTok{(v1,v2,el)}| where

  \begin{itemize}
  \tightlist
  \item
    \VERB|\NormalTok{v1}| and \VERB|\NormalTok{v2}| are vertices
    occurring in \VERB|\NormalTok{vs}|, representing a directed edge
    from \VERB|\NormalTok{v1}| to \VERB|\NormalTok{v2}|
  \item
    \VERB|\NormalTok{el}| has type \VERB|\NormalTok{EdgeLabelType}|
    (i.e.~\VERB|\NormalTok{C}|) and is the label associated with edge
    \VERB|\NormalTok{(v1,v2)}|
  \item
    an edge \VERB|\NormalTok{(v1,v2)}| occurs at most once in
    \VERB|\NormalTok{es}| (i.e.~\VERB|\NormalTok{es}| encodes a function
    from edges to edge labels)
  \end{itemize}
\end{itemize}

In terms of the abstract model, \VERB|\NormalTok{vs}| encodes
\VERB|\NormalTok{VL}| directly and, because \VERB|\NormalTok{VL}| is a
total function on \VERB|\NormalTok{V}|, it encodes \VERB|\NormalTok{V}|
indirectly. Similarly, \VERB|\NormalTok{es}| encodes
\VERB|\NormalTok{EL}| directly and \VERB|\NormalTok{E}| indirectly.

Of course, there are many other ways to represent the graph as lists.
This representation is biased for a context where, once built, the
labelled digraph is relatively static and the most frequent operations
are the retrieval of labels attached to vertices or edges. That is, it
is biased toward the Adventure game use case

\hypertarget{implementation-invariant}{%
\subsubsection{Implementation
invariant}\label{implementation-invariant}}

Given the above description, we then define the following implementation
(representation) invariant for the list-based version of the Labelled

\begin{quote}
\emph{Any Scala Digraph value
\VERB|\FunctionTok{DigraphList}\NormalTok{(vs,es)}| with abstract model
\texttt{G\ =\ (V,E,VL,EL)}, appearing in either the implicit or explicit
parameters or return value of an operation, must also satisfy the
following:}
\end{quote}

\begin{verbatim}
    (ForAll v, l :: (v,l) IN vs  <=> (v,l) IN VL ) &&
    (ForAll v1, v2, m :: (v1,v2,m) IN es  <=> ((v1,v2),m) IN EL )
\end{verbatim}

\hypertarget{scala-implementation}{%
\subsubsection{Scala implementation}\label{scala-implementation}}

See the Digraph List implementation at
\href{DigraphList.scala}{\texttt{DigraphList.scala}} and some testing
code at \href{Test_DigraphList.scala}{\texttt{Test\_DigraphList.scala}}.

In addition to the private primary constructor discussed above,
\VERB|\NormalTok{DigraphList}| implements a public zero-parameter
auxiliary constructor that returns a new empty instance of the Digraph
ADT. This is the public constructor required by the
\VERB|\NormalTok{Digraph}| specification.

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \KeywordTok{this}\NormalTok{() \{}
        \KeywordTok{this}\NormalTok{(Nil,Nil)}
\NormalTok{    \}}
\end{Highlighting}
\end{Shaded}

This constructor has the following contract, as required by the abstract
specification:

\begin{itemize}
\tightlist
\item
  Precondition: \texttt{true}
\item
  Postcondition:
  \texttt{G(this\textquotesingle{})\ ==\ (\{\},\{\},\{\},\{\})}
\end{itemize}

Auxiliary constructors in Scala must call another constructor,
eventually calling the primary constructor.

As a convenience, \VERB|\NormalTok{DigraphList}| also implements a
public copy constructor that constructs this instance to have same state
as an existing instance.

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{def} \KeywordTok{this}\NormalTok{(dg: DigraphList[A,B,C]) \{}
        \KeywordTok{this}\NormalTok{(dg.}\FunctionTok{vs}\NormalTok{,dg.}\FunctionTok{es}\NormalTok{)}
\NormalTok{    \}}
\end{Highlighting}
\end{Shaded}

This constructor has the following contract:

\begin{itemize}
\tightlist
\item
  Precondition: \texttt{G(dg)\ =\ (V,E,VL,EL)}
\item
  Postcondition: \texttt{G(this\textquotesingle{})\ ==\ G(dg)}
\end{itemize}

\hypertarget{improvements-to-the-list-implementation}{%
\subsubsection{Improvements to the list
implementation}\label{improvements-to-the-list-implementation}}

Based on the list-based design and implementation above, what
improvements should we consider?

Here are some possibilities.

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  The current list implementations of methods such as
  \VERB|\NormalTok{removeVertex}| and \VERB|\NormalTok{updateVertex}| do
  some unnecessary work with respect to the implementation invariant.
  This could be eliminated.
\item
  The data representation (i.e.~implementation invariant) could be
  changed to allow, for example, multiple occurrences of vertices in the
  vertex list. This would avoid the checks of
  \VERB|\NormalTok{hasVertex}| in \VERB|\NormalTok{addVertex}| and
  \VERB|\NormalTok{updateVertex}|. Then, as it does above,
  \VERB|\NormalTok{removeVertex}| needs to remove all occurrences of the
  vertex.

  Other functions would need to be modified accordingly so that they
  only access the first occurrence of a vertex (especially the
  \VERB|\NormalTok{allVertices}| and
  \VERB|\NormalTok{allVerticesLabels}| methods).

  A similar change could be made to the list of edges.
\item
  Most of the methods throw a \VERB|\NormalTok{sys.}\FunctionTok{error}|
  exception when the vertex they reference does not exist.

  A better Scala functional design would be to redefine these functions
  to return an \VERB|\NormalTok{Option}| or \VERB|\NormalTok{Either}|
  value. This would eliminate most of the \VERB|\NormalTok{hasVertex}|
  checks and make the functions defined on all possible inputs.

  Alternatively, we could redefine the methods to give other meaningful
  behavior in those circumstances, as suggested by some of the questions
  in the ADT specification.

  Either approach would require changes to the overall Labelled Digraph
  ADT specification and its abstract interface.
\item
  New methods could be added to the Labelled Digraph ADT---such as an
  equality check on graphs or functions to apply various graph
  algorithms.

  Alternatively, these methods could be a separate abstraction layered
  on top of the existing ADT specification.
\item
  Existing methods could be eliminated. For example, if the graph is
  only constructed and used for retrieval, then the remove and update
  functions could be eliminated.
\end{enumerate}

\hypertarget{map-implementation}{%
\subsection{Map Implementation}\label{map-implementation}}

This section gives an implementation of the ADT that uses an instance of
\VERB|\NormalTok{scala.}\FunctionTok{collection}\NormalTok{.}\FunctionTok{immutable}\NormalTok{.}\FunctionTok{HashMap}|
to map a vertex to the set of outgoing edges from that vertex,

The approach taken here is also a variation on the \emph{adjacency list}
representation of a graph.

\hypertarget{labelled-digraph-representation-1}{%
\subsubsection{Labelled digraph
representation}\label{labelled-digraph-representation-1}}

We represent the Map implementation of the Labelled Digraph ADT as a a
Scala class \VERB|\NormalTok{DigraphMap[A,B,C]}| that extends
\VERB|\NormalTok{Digraph[A,B,C]}|. (Remember that type variable
\VERB|\NormalTok{A}| is \VERB|\NormalTok{VertexType}|,
\VERB|\NormalTok{B}| is \VERB|\NormalTok{VertexLabelType}|, and
\VERB|\NormalTok{C}| is \VERB|\NormalTok{EdgeLabelType}|.)

We use the following primary constructor for this Scala class.

\begin{Shaded}
\begin{Highlighting}[]
    \KeywordTok{import}\NormalTok{ scala.}\FunctionTok{collection}\NormalTok{.}\FunctionTok{immutable}\NormalTok{.}\FunctionTok{HashMap}

    \KeywordTok{class}\NormalTok{ DigraphMap[A,B,C] }\KeywordTok{private}
\NormalTok{        (}\KeywordTok{private} \KeywordTok{val}\NormalTok{ m: HashMap[A,(B,List[(A,C)])])}
        \KeywordTok{extends}\NormalTok{ Digraph[A,B,C] \{ ... \}}
\end{Highlighting}
\end{Shaded}

This implementation represents a labeled digraph as an instance of the
Scala class \VERB|\FunctionTok{DigraphMap}\NormalTok{(m)}|, where
\VERB|\NormalTok{m}| is a Scala \VERB|\NormalTok{Map}| implemented as a
hash array mapped trie (i.e.~\VERB|\NormalTok{HashMap}|).

Note: The \VERB|\NormalTok{HashMap}| collection requires that its keys
be hashable.

An instance of \VERB|\FunctionTok{DigraphMap}\NormalTok{(m)}|
corresponds to the abstract model as follows:

\begin{itemize}
\item
  The keys for \VERB|\NormalTok{Map m}| are from
  \VERB|\NormalTok{VertexType}| (i.e.~\VERB|\NormalTok{A}|).
\item
  \VERB|\NormalTok{Map m}| is defined for all keys \VERB|\NormalTok{v1}|
  in vertex set \texttt{V} and undefined for all other possible keys.
\item
  For some vertex \VERB|\NormalTok{v1}|, the value of
  \VERB|\NormalTok{m}| at key \VERB|\NormalTok{v1}| is a pair
  \VERB|\NormalTok{(l,es)}| where

  \begin{itemize}
  \item
    \VERB|\NormalTok{l}| is an element of
    \VERB|\NormalTok{VertexLabelType}| (i.e.~\VERB|\NormalTok{B}|) and
    is the label associated with \VERB|\NormalTok{v1}|, that is,
    \VERB|\NormalTok{l == }\FunctionTok{VL}\NormalTok{(v1)}|.
  \item
    \VERB|\NormalTok{es}| is the list of all tuples
    \VERB|\NormalTok{(v2,el)}| such that \texttt{(v1,v2)\ IN\ E},
    \texttt{el\ IN\ EdgeLabelType} (i.e.~\texttt{B}\{.scala{]}), and
    \texttt{el\ ==\ EL((v1,v2))}. That is, \texttt{(v1,v2)} is an edge
    and \texttt{el} is its label.
  \end{itemize}
\end{itemize}

\hypertarget{implementation-invariant-1}{%
\subsubsection{Implementation
invariant}\label{implementation-invariant-1}}

Given the above description, we then define the following implementation
(representation) invariant for the map-based version of the Labelled
Digraph ADT:

\begin{quote}
\emph{Any Scala Digraph value
\VERB|\FunctionTok{DigraphMap}\NormalTok{(m)}| with abstract model
\texttt{G\ =\ (V,E,VL,EL)}, appearing in either the implicit or explicit
parameters or return value of an operation, must also satisfy the
following:}
\end{quote}

\begin{verbatim}
    (ForAll v1, l, es :: 
        ( m(v1) defined && m(v1) == (l,es) ) <=> 
        ( VL(v1) == l && 
        (ForAll v2, el :: (v2,el) IN es <=> 
                          EL((v1,v2)) == el) ) )
\end{verbatim}

\hypertarget{scala-implementation-1}{%
\subsubsection{Scala implementation}\label{scala-implementation-1}}

See the Digraph Map implementation at
\href{DigraphMap.scala}{\texttt{DigraphMap.scala}} and some testing code
at \href{Test_DigraphMap.scala}{\texttt{Test\_DigraphMap.scala}}.

As with the Digraph List implementation, the Map implementation has two
auxiliary constructors---a zero-parameter constructor and a copy
constructor.

\hypertarget{improvements-to-the-map-implementation}{%
\subsubsection{Improvements to the map
implementation}\label{improvements-to-the-map-implementation}}

All the improvements suggested for the list-based implementation apply
to the map-based implementation except for the first.

For large graphs, the map-based implementation should perform better
than the list-based implementation.

For large graphs with many outgoing edges on each vertex, it might be
useful to implement the edge-list itself with a
\VERB|\NormalTok{HashMap}|.

Alternatively, a \texttt{HashMap} could use use pairs
\VERB|\NormalTok{(v1,v2)}| for its keys. This would give a more direct
analog to an array-based adjacency matrix representation. The vertex
labels could be represented separately by a list or map that associates
a vertex with its label.

\hypertarget{mealy-machine-simulator-project}{%
\subsection{Mealy Machine Simulator
Project}\label{mealy-machine-simulator-project}}

In this project, you are asked to design and implement Scala ``modules''
to represent Mealy Machines and to simulate their execution.

\hypertarget{mealy-machine}{%
\subsubsection{Mealy Machine}\label{mealy-machine}}

A Mealy Machine is a useful abstraction for simple controllers that
listen for input events and respond by generating output events. For
example in an automobile application, the input might be an event such
as ``fuel level low'' and the output might be command to ``display
low-fuel warning message''.

In the theory of computation, a \emph{Mealy Machine} is a
\emph{finite-state automaton} whose output values are determined both by
its current state and the current input. It is a \emph{deterministic
finite state transducer} such that, for each state and input, at most
one transition is possible.

Appendix A of the Linz textbook {[}Linz 2017{]} defines a Mealy Machine
mathematically by a tuple

\begin{quote}
\(M = (Q,\Sigma,\Gamma,\delta,\theta,q_{0})\)
\end{quote}

where

\begin{quote}
\(Q\) is a finite set of internal states\\
\(\Sigma\) is the input alphabet (a finite set of values)\\
\(\Gamma\) is the output alphabet (a finite set of values)\\
\(\delta: Q \times \Sigma \longrightarrow Q\) is the transition
function\\
\(\theta: Q \times \Sigma \longrightarrow \Gamma\) is the output
function\\
\(q_{0}\) is the initial state of \(M\) (an element of \(Q\))
\end{quote}

In an alternative formulation, the transition and output functions can
be combined into a single function:

\begin{quote}
\(\delta: Q \times \Sigma \longrightarrow Q \times \Gamma\)
\end{quote}

We often find it useful to picture a finite state machine as a
\emph{transition graph} where the states are mapped to vertices and the
transition function represented by directed edges between vertices
labelled with the input and output symbols.

\hypertarget{mealy-machine-exercises}{%
\subsubsection{Mealy Machine Exercises}\label{mealy-machine-exercises}}

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  Specify, design, and implement a general representation for a Mealy
  Machine as a set of Scala definitions implementing an abstract data
  type. It should hide the representation of the machine behind an
  abstract interface and should have, at least, the following public
  operations.

  \begin{itemize}
  \item
    Constructor \VERB|\FunctionTok{MealyMachine}\NormalTok{(s)}| creates
    a new machine with initial (and current) state \VERB|\NormalTok{s}|
    and no transitions.
  \item
    Mutator method \VERB|\FunctionTok{addState}\NormalTok{(s)}| adds a
    new state \VERB|\NormalTok{s}| to this machine and returns an
    \VERB|\NormalTok{Either}| wrapping the modified machine or an error
    message.
  \item
    Mutator method
    \VERB|\FunctionTok{addTransition}\NormalTok{(s1,in,out,s2)}| adds a
    new transition to this machine and returns an
    \VERB|\NormalTok{Either}| wrapping the modified machine or an error
    message. From state \VERB|\NormalTok{s1}| with input
    \VERB|\NormalTok{in}|, the modified machine outputs
    \VERB|\NormalTok{out}| and transitions to state
    \VERB|\NormalTok{s2}|.
  \item
    Mutator method \VERB|\NormalTok{addResets}| adds all reset
    transitions to this machine and returns the modified machine. This
    operation makes the transition function a total function by adding
    any missing transitions from a state back to the initial state.
  \item
    Mutator method \VERB|\FunctionTok{setCurrent}\NormalTok{(s)}| sets
    the current state of this machine to \VERB|\NormalTok{s}| and
    returns an \VERB|\NormalTok{Either}| wrapping the modified machine
    or an error message.
  \item
    Accessor method \VERB|\NormalTok{getCurrent}| returns the current
    state of this machine.
  \item
    Accessor method \VERB|\NormalTok{getStates}| returns a list of the
    elements of the state set of this machine.
  \item
    Accessor method \VERB|\NormalTok{getInputs}| returns a list of the
    input set of this machine.
  \item
    Accessor method \VERB|\NormalTok{getOutputs}| returns a list of the
    output set of this machine.
  \item
    Accessor method \VERB|\NormalTok{getTransitions}| returns a list of
    the transition set of this machine. Tuple
    \VERB|\NormalTok{(s1,in,out,s2)}| occurs in the returned list if and
    only if, from state \VERB|\NormalTok{s1}| with input
    \VERB|\NormalTok{in}|, the machine outputs \VERB|\NormalTok{out}|
    and moves to state \VERB|\NormalTok{s2}|.
  \item
    Accessor method
    \VERB|\FunctionTok{getTransitionsFrom}\NormalTok{(s)}| returns an
    \VERB|\NormalTok{Either}| wrapping a list of the set of transitions
    enabled from state \VERB|\NormalTok{s}| of this machine or an error
    message.
  \end{itemize}

  Note: It is possible to use a Labelled Digraph ADT module in the
  implementation of the Mealy Machine. A state is a vertex of the graph,
  transition is an edge of the graph, and an \VERB|\NormalTok{(in,out)}|
  is a label for an edge.
\item
  Given the above implementation for a Mealy Machine ADT, design and
  implement a separate Scala module that simulates the execution of a
  Mealy Machine. It should have, at least, the following public
  operations.

  \begin{itemize}
  \item
    Mutator \VERB|\FunctionTok{move}\NormalTok{(m,in)}| moves machine
    \VERB|\NormalTok{m}| from the current state given input
    \VERB|\NormalTok{in}| and returns an \VERB|\NormalTok{Either}|
    wrapping a tuple \VERB|\NormalTok{(mm,out)}| or an error message.
    The tuple gives the modified machine \VERB|\NormalTok{mm}| and the
    output \VERB|\NormalTok{out}|.
  \item
    Mutator method \VERB|\FunctionTok{simulate}\NormalTok{(m,ins)}|
    simulates execution of machine \VERB|\NormalTok{m}| from its current
    state through a sequence of moves for the inputs in list
    \VERB|\NormalTok{ins}| and returns an \VERB|\NormalTok{Either}|
    wrapping a tuple \VERB|\NormalTok{(mm,outs)}| or an error message.
    The tuple gives the modified machine \VERB|\NormalTok{mm}| after the
    sequence of moves and the output list \VERB|\NormalTok{outs}|.
  \end{itemize}
\item
  Implement a Scala abstract data type that uses a different
  representation for the Mealy Machine. Make sure the simulator module
  still works correctly.
\end{enumerate}

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

I specified the Doubly Labelled Digraph ADT for Assignment \#1 in CSci
556 (Multiparadigm Programming) in Spring 2015. This assignment was
motivated by underlying data structure for the Wizard's Adventure Game
from {[}Barski 2011{]}. I developed the list- and map-based Haskell
implementations as my solution for that assignment. In addition, I
developed a list-based implementation in Elixir and used it to implement
the Adventure game. In Spring 2016, I developed list- and map-based
Scala implementations for CSci 555 (Functional Programming).

In Spring 2016, I defined the Mealy Machine Simulator as a programming
assignment in the Scala-based CSci 555 (Functional Programming) course.

In Spring 2017, I created a Labelled Digraph ADT document by adapting
and revising comments from the Haskell implementations of the Labelled
Digraph abstract data type. I also included some content from my notes
on Data Abstraction {[}Cunningham 2019{]}. I also revised the Mealy
Machine assignment description to create a Mealy Machine Exercise
document.

In 2018, I merged and revised these documents to become a new Chapter
23, Data Abstraction Revisited, in the textbook \emph{Exploring
Languages with Interpreters and Functional Programming (ELIFP)}.

In 2019, I adapted Chapter 23 and parts of Chapter 7 of ELIFP and the
Scala-based source code comments to develop these notes.

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

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

\begin{description}
\tightlist
\item[{[}Barski 2011{]}:]
Conrad Barski. Building a Text Game Engine, \emph{Land of Lisp: Learn to
Program in Lisp, One Game at a Time}, pp.~69-84, No Starch Press, 2011.
(The Common Lisp example in this chapter is similar to the classic
Adventure game; the underlying data structure is a labelled digraph.)
\item[{[}Britton 1981{]}:]
K. H. Britton, R. A. Parker, and D. L. Parnas. A Procedure for Designing
Abstract Interfaces for Device Interface Modules, In \emph{Proceedings
of the 5th International Conference on Software Engineering},
pp.~195-204, March 1981.
\item[{[}Brooks 1986{]}:]
F. P. Brooks Jr.~No Silver Bullet---Essence and Accidents in Software
Engineering, \emph{Information Processing}, Elsevier Science,
pp.~1068-1076, 1986.
\item[{[}Brooks 1995{]}:]
F. P. Brooks Jr.~`No Silver Bullet' Refired, Chapter 17, In The
\emph{Mythical Man Month}, Anniversary Edition, 1995.
\item[{[}Cunningham 2019{]}:]
H. Conrad Cunningham.
\href{../../DataAbstraction/DataAbstraction.html}{\emph{Notes on Data
Abstraction}}, 1996-2019.
\item[{[}Cunningham 2019b{]}:]
H. Conrad Cunningham.
\href{../RecursionStyles/RecursionStylesScala.html}{\emph{Recursion
Styles, Correctness, and Efficiency (Scala Version)}}, 2019.
\item[{[}Dale 1996{]}:]
Nell Dale and Henry M. Walker. Directed Graphs or Digraphs, Chapter 10,
In \emph{Abstract Data Types: Specifications, Implementations, and
Applications}, pp.~439-469, D. C. Heath \& Co, 1996.
\item[{[}Linz 2017{]}:]
Peter Linz. \emph{Formal Languages and Automata}, 6th Edition, Jones \&
Bartlett, 2017.
\item[{[}Meyer 1997{]}:]
Bertrand Meyer. \emph{Object-Oriented Program Construction}, Second
edition, Prentice Hall, 1997.
\item[{[}Parnas 1972{]}:]
D. L. Parnas. On the Criteria to Be Used in Decomposing Systems into
Modules, \emph{Communications of the ACM}, Vol. 15, No.~12,
pp.1053-1058, 1972.
\item[{[}Parnas 1976{]}:]
D. L. Parnas. On the Design and Development of Program Families,
\emph{IEEE Transactions on Software Engineering}, Vol. SE-2, No.~1, pp.
1-9, March 1976.
\item[{[}Parnas 1978{]}:]
D. L. Parnas. Some Software Engineering Principles, \emph{Infotech State
of the Art Report on Structured Analysis and Design}, Infotech
International, 10 pages, 1978. Reprinted in \emph{Software Fundamentals:
Collected Papers by David L. Parnas}, D. M. Hoffman and D. M. Weiss,
editors, Addison-Wesley, 2001.
\item[{[}Parnas 1979{]}:]
D. L. Parnas. Designing Software for Ease of Extension and Contraction,
\emph{IEEE Transactions on Software Engineering}, Vol. SE-5, No.~1,
pp.~128-138, March 1979.
\item[{[}Parnas 1985{]}:]
D. L. Parnas, P. C. Clements, and D. M. Weiss. The Modular Structure of
Complex Systems, \emph{IEEE Transactions on Software Engineering}, Vol.
SE-11, No.~3, pp.~259-266, March 1985.
\item[{[}Weiss 2001{]}:]
D. M. Weiss. Introduction: On the Criteria to Be Used in Decomposing
Systems into Modules, In \emph{Software Fundamentals: Collected Papers
by David L. Parnas}, D. M. Hoffman and D. M. Weiss, editors,
Addison-Wesley, 2001.
\end{description}

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

TODO: Update

Data abstraction; module, goals of modularization (comprehensibility,
independent development, changeability), information hiding, secret,
encapsulation, contract (precondition, postcondition, invariant),
interface, abstract interface; client-supplier relationship, design
criteria for interfaces; abstract data type (ADT), instance;
specification of ADTs using name, sets, signatures, and semantics;
constructor, accessor, mutator, and destructor operations; axiomatic and
constructive semantics; abstract model, interface and implementation
invariant; using mathematical concepts to model the data abstraction;
graph, digraph, labelled graph, multigraph, set, sequence, total and
partial functions, relation; adventure game; use of Scala trait and
generics to define ADT interface, Scala constructors (private,
auxiliary), builtin List and Map (HashMap) data structures; adjacency
matrix, adjacency list.

Mealy Machine, simulator, finite-state automaton (machine),
deterministic finite state transducer, state, transition, transition
graph.

\end{document}
