\documentclass[]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
\else % if luatex or xelatex
  \ifxetex
    \usepackage{mathspec}
  \else
    \usepackage{fontspec}
  \fi
  \defaultfontfeatures{Ligatures=TeX,Scale=MatchLowercase}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
% use microtype if available
\IfFileExists{microtype.sty}{%
\usepackage[]{microtype}
\UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\PassOptionsToPackage{hyphens}{url} % url is loaded by hyperref
\usepackage[unicode=true]{hyperref}
\hypersetup{
            pdftitle={CSci 556: Multiparadigm Programming Carrie's Candy Bowl Semantics},
            pdfauthor={H. Conrad Cunningham},
            pdfborder={0 0 0},
            breaklinks=true}
\urlstyle{same}  % don't use monospace font for urls
\IfFileExists{parskip.sty}{%
\usepackage{parskip}
}{% else
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{0}
% 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}

\title{CSci 556: Multiparadigm Programming\\
Carrie's Candy Bowl Semantics}
\author{H. Conrad Cunningham}
\date{27 February 2017}

\begin{document}
\maketitle

{
\setcounter{tocdepth}{4}
\tableofcontents
}
Copyright (C) 2014, 2017, H. Conrad Cunningham

\textbf{Acknowledgements:} I wrote the first version of these notes in
Fall 2013 as comments in Lua code for the Carrie's Candy Bowl case
study. This code was for an extended solution to a problem given on a
take-home examination. In Fall 2014, I revised the comments and used
them as the basis for separate documents.

In Spring 2017, I revised the documents and reformatted them to use
Markdown, restated the semantics to use the ``better semantics''
documented in the code, and partially updated the document for use in a
multi-language context.

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

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

\section{Carrie's Candy Bowl ADT}\label{carries-candy-bowl-adt}

\subsection{Introduction}\label{introduction}

Carrie, the Department's Administrative Assistant, has a candy bowl on
her desk. Often she fills this bowl with pieces of candy, which are
quickly consumed by students and professors.

This case study describes the candy bowl as an abstract data type (ADT)
suitable for implementation as Lua modules.

Notes:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  This problem description differs slightly from the descriptions of the
  problem used in later Scala- and Haskell-based classes.
\item
  This problem description allows the implementations to use mutable
  state or to use only immutable state. Thus the specification may be
  imprecise about the possible effects of mutator operations.
\end{enumerate}

\subsection{Specifying Semantics}\label{specifying-semantics}

\subsubsection{Operations}\label{operations}

We identify four basic kinds of operations on abstract data types:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  A \emph{constructor} (also called a creator, factory, or producer)
  operation creates a new instance of the ADT.
\item
  A \emph{mutator} (also called a setter, modifier, or command)
  operation returns the input instance with its state changed.
\item
  An \emph{accessor} (also called a getter, observer, or query)
  operation accesses input instance's state and returns a value that
  characterizes the instance.
\item
  A \emph{destructor} operator destroys an instance and ``releases'' its
  resources.
\end{enumerate}

An ADT can be implemented in various ways. In most circumstances, it is
best to keep an accessor as a pure function. That is, an accessor should
not modify the state of the input instance in any observable manner.
However, a mutator may be a pure function--returning a modified copy of
the input instance--or it may be impure--directly modifying the value of
the input instance.

In the imperative, object-oriented language Java, an abstract data type
is typically defined using an \texttt{abstract\ class} or
\texttt{interface} and implemented using a concrete \texttt{class} that
extends the abstract class or implements the interface. The various ADT
operations are the public methods of the class. An instance of the ADT
is an instance of the concrete class whose instance variables hold the
instance's state.

In the purely functional language Haskell, an abstract data type is
typically implemented using a \texttt{module} with definitions of its
types and functions. The module explicitly exports the public types and
operations and hides other aspects of the specific implementation.
Constructor functions create and return new instances of the ADT. These
instances must be explicitly passed into the accessor, mutator, and
destructor operations. A mutator operation returns a modified copy of
the input instance. Currently, the module system does not support
multiple implementations of the same interface; thus the overall
abstract data type is represented by a set of modules all having the
same set of exported operations.

Lua is a minimalistic language, but it is one that has powerful,
flexible features. It is dynamically typed and mostly imperative. It
offers a number of ways to implement abstract data types. As a result,
it is challenging to specify ADTs formally.

This case study assumes we are implementing the ADT as a Lua module that
exports functions for the public operations. However, the case study
seeks to enable a number of different implementation techniques.

\subsubsection{Contracts}\label{contracts}

The module defines the semantics of the Candy Bowl abstract data type
(ADT) using

\begin{itemize}
\item
  \emph{invariant} assertions to characterize valid states of its
  instances (between ADT operation calls)
\item
  \emph{precondition} and \emph{postcondition} assertions to
  characterize the behavior of ADT operations
\end{itemize}

These assertions (or predicates or Boolean functions) are logical
statements that must hold (i.e., be true) for an ADT instance to be
valid.

If the precondition of an operation holds, then the operation must
terminate with its postcondition true. The precondition characterizes
valid values of the input arguments and other aspects of the program's
state at the time of the call. The postcondition characterizes the value
of the return value and any other effects caused by the operation. The
postcondition often states the output values in terms of the input
state.

The invariants must hold for an instance after execution of its
constructor, before and after execution of mutator and accessor
operations, and before execution of any destructor operation. Invariants
are implicitly conjuncted (i.e., ANDed) to the preconditions and
postconditions of the ADT's operations.

An ADT \emph{interface invariant} specifies the valid value (i.e.,
state) of an ADT instance in terms of an abstract model of the ADT (and
perhaps of primitive operation in the module's interface). It must be
the same for any implementation of the ADT. It does not reference the
state of any implementation variables.

An ADT \emph{implementation invariant} complements the interface
invariant by defining the abstract model's state in terms of the state
of an implementation's concrete variables and data structures.

We consider the invariants and the preconditions and the postconditions
of all public operations of the ADT operations to form the
\emph{contract} between the users and developers of the ADT.

\subsubsection{Concepts and notation}\label{concepts-and-notation}

We use the following mathematical and logical concepts and notation to
express the semantics of the ADT and its operations. Here, we use
notation that can be typed into comments for computer programs, not the
notation that would be typeset in a mathematics or logic textbook. The
logic notation follows that popularized by Edsger Dykstra, David Gries,
and others. (We do not use all of these concepts and notation in
specification of the Candy Bowl abstract data type.)

The following gives an informal explanation of the concepts and
notation.

\begin{itemize}
\item
  \texttt{(ForAll\ x\ :\ D(x)\ ::\ R(x))} denotes universal
  quantification. It is true if and only if assertion \texttt{R(x)} is
  true for \emph{all} values \texttt{x} that satisfy assertion
  \texttt{D(x)}. If \texttt{D(x)} is omitted, then it does not constrain
  \texttt{x}.

  We can extend this notation to quantify over tuples of values such as
  in \texttt{(ForAll\ x,y,z\ :\ D(x,x,z)\ ::\ R(x,y,z))}.
\item
  \texttt{(Exists\ x\ :\ D(x)\ ::\ R(x))} denotes existential
  quantification. It is true if and only if assertion \texttt{R(x)} is
  true for \emph{at least one} value \texttt{x} that satisfies assertion
  \texttt{D(x)}. If \texttt{D(x)} is omitted, then it does not constrain
  \texttt{x}.
\item
  \texttt{(\#\ x\ :\ D(x)\ ::\ R(x))} denotes a count of all values
  \texttt{x} that satisfies assertion \texttt{D(x)} and assertion
  \texttt{R(x)}.
\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
  A \emph{set} is an unordered collection of elements without
  duplicates. We use typical notation and operations on sets.
\item
  A \emph{bag} (also called a \emph{multiset}) is an unordered
  collection of elements in which each value may occur one or more
  times. Here we use the following notation.

  \begin{itemize}
  \item
    \texttt{\{\textbar{}\ \textbar{}\}} denotes the empty bag.
  \item
    \texttt{\{\textbar{}\ 2,\ 3,\ 2,\ 1\ \textbar{}\}} denotes a bag
    with four elements including two 2's, one 3, and one 1. The order is
    not significant! There may be one or more occurrences of an element.
  \item
    A set can be considered a bag with at most one occurrence of an
    element.
  \item
    We can formalize a bag as a function from the set of elements to the
    natural numbers (i.e., nonnegative integers).
  \end{itemize}
\item
  A \emph{sequence} is an ordered collection of elements in which each
  value may occur one or more times.
\item
  A \emph{type} consists of a set of values and a set of operations. In
  some circumstances, we consider the type as a set of values.
\item
  Membership. For a collection (i.e., a set, bag, sequence, or type)
  \texttt{C}, \texttt{x\ IN\ C} if only if element \texttt{x} occurs in
  collection \texttt{C}.
\item
  \texttt{OCCURENCES(x,C)} denotes the number of times element
  \texttt{x} appears in collection \texttt{C}. For a set, this will be
  integer 0 or 1. For a bag or sequence, there many be any nonnegative
  number of occurrences.
\item
  \texttt{CARDINALITY(C)} denotes the total number of occurrences of all
  elements in a collection \texttt{C}.
\item
  \texttt{REPEAT(e,n)} denotes a bag containing exactly \texttt{n}
  occurrences of \texttt{e} or an empty bag if
  \texttt{n\ \textless{}\ 1}.
\item
  Union.

  \begin{itemize}
  \item
    For sets \texttt{C} and \texttt{D}, an element occurs in the set
    \texttt{C\ UNION\ D} if and only if it occurs in \texttt{C} or in
    \texttt{D} (or both).
  \item
    Similarly, for bags \texttt{C} and \texttt{D}, an element has
    exactly \texttt{n} occurrences in bag \texttt{C\ UNION\ D} if and
    only if \texttt{n} is the \emph{maximum} of the number of its
    occurrences in \texttt{C} and in \texttt{D}

    \texttt{\{\textbar{}\ 1,\ 1,\ 2,\ 1\ \}\}\ UNION\ \{\textbar{}\ 2,\ 1,\ 1\ \textbar{}\}}
    yields \texttt{\{\textbar{}\ 1,\ 1,\ 1,\ 2\ \textbar{}\}}.
  \end{itemize}
\item
  Sum.

  \begin{itemize}
  \item
    For bags \texttt{C} and \texttt{D}, an element has exactly
    \texttt{n} occurrences in bag \texttt{C\ +\ D} if and only if
    \texttt{n} is the \emph{sum} of the number of occurrences in
    \texttt{C} and in \texttt{D}.

    \texttt{\{\textbar{}\ 1,\ 1,\ 2,\ 1\ \}\}\ +\ \{\textbar{}\ 2,\ 1,\ 1\ \textbar{}\}}
    yields
    \texttt{\{\textbar{}\ 1,\ 1,\ 1,\ 1,\ 1,\ 2,\ 2\ \textbar{}\}}.
  \end{itemize}
\item
  Intersection.

  \begin{itemize}
  \item
    For sets \texttt{C} and \texttt{D}, an element occurs in set
    \texttt{C\ INTERSECT\ D} if and only if it occurs in both \texttt{C}
    and \texttt{D}.
  \item
    Similarly, for bags \texttt{C} and \texttt{D}, an element has
    exactly \texttt{n} occurrences in bag \texttt{C\ INTERSECT\ D} if
    and only if \texttt{n} is the \emph{minimum} of the number of
    occurrences in \texttt{C} and in \texttt{D}.

    \texttt{\{\textbar{}\ 1,\ 1,\ 2,\ 1\ \}\}\ INTERSECT\ \{\textbar{}\ 2,\ 1,\ 1\ \textbar{}\}}
    yields \texttt{\{\textbar{}\ 1,\ 1,\ 2\ \textbar{}\}}.
  \end{itemize}
\item
  Difference.

  \begin{itemize}
  \item
    For sets \texttt{C} and \texttt{D}, an element occurs in set
    \texttt{C\ -\ D} if and only if it occurs in \texttt{C} but not in
    \texttt{D}.
  \item
    Similarly, for bags \texttt{C} and \texttt{D}, an element has
    exactly \texttt{n} occurrences in bag \texttt{C\ -\ D} if and only
    if the elements occurs exactly \texttt{n} more times in \texttt{C}
    than in \texttt{D},

    \texttt{\{\textbar{}\ 1,\ 1,\ 2,\ 1\ \}\}\ -\ \{\textbar{}\ 2,1,1\ \textbar{}\}}
    yields \texttt{\{\textbar{}\ 1\ \textbar{}\}}.
  \end{itemize}
\item
  Subset.

  \begin{itemize}
  \item
    For sets \texttt{C} and \texttt{D}, \texttt{C\ SUBSET\_OF\ D}
    denotes that all the elements of \texttt{C} also occur in
    \texttt{D}.
  \item
    For bags \texttt{C} and \texttt{D}, \texttt{C\ SUBSET\_OF\ D}
    denotes that if any element has \texttt{n} occurrences in \texttt{C}
    and \texttt{m} occurrences in \texttt{D} then
    \texttt{n\ \textless{}=\ m}.
  \end{itemize}
\item
  TODO: Define Cartesian products, tuples, relations, functions?
\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 quantification as
  \texttt{\{\ (x,c)\ ::\ c\ IN\ some\_domain\ \}}.
\item
  A \emph{function} is a special case of a \emph{relation} and relation
  is a set of ordered pairs (tuples). We sometimes manipulate functions
  or relations using set notation for convenience.
\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}

\subsection{Candy Bowl Specification}\label{candy-bowl-specification}

\subsubsection{Abstract model}\label{abstract-model}

We represent a Candy Bowl instance as a mathematical bag of
\texttt{CandyType} elements. If \texttt{bowl} is some representation of
the Candy Bowl in the program, then the notation \texttt{Bag(bowl)}
denotes the corresponding abstract model.

\subsubsection{Interface invariant}\label{interface-invariant}

Any valid instance of the Candy Bowl must satisfy the bag properties.

All Candy Bowl instances passed explicitly or implicitly to an ADT
operation or returned explicitly or implicitly must be valid.

\subsubsection{Constructive semantics}\label{constructive-semantics}

The preconditions and postconditions of each ADT operation are given
below. These are part of the (implementation-independent) specification
of the ADT.

We parameterize the specification with a domain set \texttt{CandyType}.
We assume that assertion \texttt{validCandyType(c)} holds if and only if
\texttt{c} represents a candy type supported by the module.

For convenience, we assume assertion \texttt{validCandyBowl(b)} holds if
and only if \texttt{b} represents a bowl that satisfies the invariants.
(Given our assumption that invariants are implicitly conjuncted with
both preconditions and postconditions, use of this should not be
necessary in most circumstances. However, we use it below to make the
intention clear.)

In a postcondition:

\begin{itemize}
\tightlist
\item
  \texttt{Arg\_XXX} denotes the value of explicit or implicit argument
  variable \texttt{XXX} at the time of the call of the operation.
\item
  \texttt{Return} denotes the value returned explicitly by a operation's
  function.
\item
  \texttt{Unchanged(Arg\_b)} denotes that the value of variable
  \texttt{b} is not changed by the operation's execution.
\end{itemize}

Now, let's examine the operations.

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  Constructor function \texttt{CandyBowl(bowl)} returns a new candy
  bowl. If the argument \texttt{bowl} is (Lua value) \texttt{nil} or
  unspecified, then the new bowl is empty; otherwise, the new bowl has
  the same elements as the \texttt{bowl} argument.

  Note: The optional argument \texttt{bowl} was not in the original Fall
  2013 problem description; I added it to illustrate use of optional
  arguments. If an argument is omitted, then the function sees it has
  having a \texttt{nil} value. For other languages, the one-argument
  function might need to be separate from the zero-argument function.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
bowl == nil OR validCandyBowl(bowl)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(if Arg_bowl == nil 
    then CARDINALITY(Bag(Return)) == 0
    else Bag(Return) == Bag(Arg_bowl))
&& Unchanged(Bag(Arg_bowl))
\end{verbatim}
  \end{itemize}

  Discussion: The one-argument operation is intended to be a ``copy''
  constructor. (a) The new bowl should be a copy of the input bowl, not
  just another reference to the input (i.e., an alias). (b) The input
  \texttt{bowl} should not be changed.

  These are tricky to specify formally because of Lua's dynamic typing,
  its passing of its \texttt{table} data structure by reference, and the
  relative openness of its \texttt{table} data structure to
  modification.

  The \texttt{Unchanged(Bag(Arg\_bowl))} conjunct on the postcondition
  addresses second intention.

  For now, this specification does not address the copying/aliasing
  issue. Even if we require \texttt{Arg\_bowl} and \texttt{Return} to
  denote different addresses, there is no good way to state that they do
  not share components.
\item
  Accessor function \texttt{has(bowl,candyType)} returns true if and
  only if \texttt{bowl} contains one or more pieces of type
  \texttt{candyType} candy. The argument \texttt{bowl} is not modified.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validCandyBowl(bowl) && validCandyType(candyType)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Return == OCCURENCES(candyType,Arg_bowl) > 0
&& Unchanged(Arg_bowl)
\end{verbatim}
  \end{itemize}
\item
  Mutator function \texttt{put(bowl,candyType,n)} adds integer
  \texttt{n} pieces of \texttt{candyType} candy to the argument
  \texttt{bowl}. \texttt{n} defaults to 1 if \texttt{nil} or
  unspecified.

  Note: The optional argument \texttt{n} was not in the original Fall
  2013 problem description. For other languages, the three-argument
  version might need to be a separate function from the two-argument
  function.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validCandyType(candyType) && (n == nil or n > 0)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
if n == nil
then Bag(Return) == Bag(Arg_bowl) + {| candyType |}
else Bag(Return) == Bag(Arg_bowl) + REPEAT(c,n)
\end{verbatim}
  \end{itemize}

  Discussion: The original problem specification allows this function to
  modify its \texttt{bowl} argument. We can add conjunct

\begin{verbatim}
    Unchanged(Arg_bowl)
\end{verbatim}

  to the postcondition to require a function without side effects.
  (Function \texttt{put} in the implementation modifies its argument;
  alternative function \texttt{putcp} returns a modified ``shallow''
  copy.)
\item
  Mutator function \texttt{take(bowl,candyType)} removes one piece of
  \texttt{candyType} candy from the argument \texttt{bowl}.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validCandyBowl(bowl_ && validCandyType(candyType) && 
OCCURRENCES(candyType,Bag(Arg_bowl)) > 0
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Bag(Return) == Bag(Arg_bowl) - {| candyType |}
\end{verbatim}
  \end{itemize}

  Discussion: The original problem specification allows this function to
  modify its \texttt{bowl} argument. We can add conjunct

\begin{verbatim}
    Unchanged(Arg_bowl)
\end{verbatim}

  to the postcondition to require a function without side effects.
  (Function \texttt{take} in the implementation modifies its argument;
  alternative function \texttt{takecp} returns a modified ``shallow''
  copy.)
\item
  Accessor function \texttt{howMany(bowl,candyType)} returns the number
  of pieces of candy that are in the \texttt{bowl} overall if
  \texttt{candyType} is nil; otherwise, the function returns the count
  of the pieces of \texttt{candyType} candy that are in the bowl.

  Note: Argument \texttt{candyType} was not optional in the original
  Fall 2013 problem description. For other languages, the one- and
  two-argument functions would need to be separate.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validCandyBowl(bowl) &&
(candyType == nil OR validCandyType(candyType))
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
( if candyType == nil 
  then Return == CARDINALITY(Bag(Arg_bowl))
  else Return == OCCURRENCES(candyType,Bag(Arg_bowl) )
&& Unchanged(Arg_bowl)
\end{verbatim}
  \end{itemize}
\item
  Accessor function \texttt{isEmpty(bowl)} returns true if and only if
  the \texttt{bowl} is empty.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validCandyBowl(bowl)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Return == CARDINALITY(Bag(Arg_bowl)) == 0 
&& Unchanged(Arg_bowl)
\end{verbatim}
  \end{itemize}
\item
  Accessor function \texttt{inventory(bowl)} returns a list-style table
  of pairs \texttt{\{candyType,\ count\}}.

  Note: This function describes a specific Lua data structure to be
  returned, so the specification uses Lua notation.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validCandyBowl(bowl)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
validInventory(Return) &&
(ForAll c,n: OCCURRENCES(c,Bag(Arg_bowl)) == n && n > 0 ::
    (Exists i: i > 0 :: Return[i] == {c,n}) )) &&
(ForAll i,c,n: 1 <= i <= #Return && Return[i] == {c,n} ::
    OCCURRENCES(c,Bag(Arg_bowl))== n)) &&
Unchanged(Arg_bowl)
\end{verbatim}

    where

\begin{verbatim}
validInventory(inv) == 
    inv ~= nil && type(inv) = "table" &&
    (ForAll i: i < 1 or i > #inv :: inv[i] == nil) &&
    (ForAll i: 1 <= i <= #inv ::
        (Exists c,n: inv[i] == {c,n}:: 
                      validCandyType(c) && n > 0) )
    && 
    (ForAll i: 2 <= i <= #inv :: inv[i-1][1] < inv[i][1]) )
\end{verbatim}
  \end{itemize}

  For example, if \texttt{candyType} is denoted by a string and there
  are two Snickers and one Hershey Kiss in the bowl, then the list
  returned would be something like
  \texttt{\{\ \{\textquotesingle{}Hershey\ Kiss\textquotesingle{},\ 1\},\ \ \{\textquotesingle{}Snickers\textquotesingle{},\ 2\}\ \}}.
\item
  Constructor function \texttt{toBowl(inv)} takes an inventory
  \texttt{inv} (as returned by the \texttt{inventory} operation and
  returns the corresponding bowl.

  Note: This operation was not in the original problem description. It
  taskes a specific Lua data structure as input, so the specification
  uses Lua notation.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validInventory(inv)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
(ForAll c,n: OCCURRENCES(c,Bag(Return)) == n && n > 0 :: 
    (Exists i: 1 <= i && i <= #inv :: inv[i] == {c,n}) ))  &&
(ForAll i,c,n: 1 <= i <= #inv && inv[i] == {c,n} :: 
    OCCURRENCES(c,Bag(Return)) == n)) &&
Unchanged(inv) 
\end{verbatim}
  \item
    Property:

\begin{verbatim}
(ForAll bowl :: validCandyBowl(bowl) ::
    Bag(toBowl(inventory(bowl))) == Bag(bowl) )
\end{verbatim}
  \end{itemize}
\item
  Mutator function \texttt{combine(bowl1,bowl2)} returns the bowl
  resulting from pouring \texttt{bowl1} and \texttt{bowl2} together to
  form a new bowl.

  \begin{itemize}
  \item
    Precondition:

\begin{verbatim}
validCandyBowl(bowl1) && validCandyBowl(bowl2)
\end{verbatim}
  \item
    Postcondition:

\begin{verbatim}
Bag(Return) == Bag(Arg_bowl1) + Bag(Arg_bowl2)
\end{verbatim}
  \end{itemize}

  Discussion: The original problem specification allows this function to
  modify the \texttt{bowl1} and \texttt{bowl2} arguments. We can add
  conjuncts

\begin{verbatim}
    Unchanged(Arg_bowl1) && Unchanged(Arg_bowl2)
\end{verbatim}

  to the postcondition to require a function without side effects.
  (Function \texttt{combine} in the implementation modifies its first
  arguments; alternative function \texttt{combine2} returns a modified
  ``shallow'' copy.)
\end{enumerate}

For other languages, the aspects of the contracts related to the
abstract bag model should be the same. Of course, references to specific
Lua features such its \texttt{table} data structure, value \texttt{nil},
and optional arguments would need to be changed appropriately.

\subsection{Data Representations}\label{data-representations}

\subsubsection{Lua hashed Version}\label{lua-hashed-version}

The first version of the module represents the Candy Bowl ADT with a Lua
hash table that maps \texttt{candyType} key values to the count of the
pieces of that type. In addition, the special key \texttt{SIZE} maps to
the count of the total number of pieces in the table.

An ADT \emph{implementation invariant} for Candy Bowl \texttt{bowl} can
be stated as

\begin{verbatim}
    (ForAll c: validCandyType(c) :: 
        if bowl[c] ~= nil 
          then bowl[c] == OCCURRENCES(c,Bag(bowl))
          else OCCURRENCES(c,Bag(bowl)) == 0)
    && bowl[SIZE] == CARDINALITY(Bag(bowl))
\end{verbatim}

where
\texttt{validCandyType(c)\ ==\ (c\ \textasciitilde{}=\ nil\ \&\&\ c\ \textasciitilde{}=\ SIZE)}.

\subsubsection{Lua list Version}\label{lua-list-version}

The second version of the Candy Bowl ADT module has the same interface
as the hashed version, but it uses a different internal data
representation. This version uses with an unsorted, list-style table of
\texttt{candyType}s.

An ADT \emph{implementation invariant} for Candy Bowl \texttt{bowl} can
be stated as

\begin{verbatim}
  (ForAll i : 1 <= i <= #bowl :: validCandyType(bowl[i]))  &&
  (ForAll c : validCandyType(c) ::
    howMany(bowl,c) == (Sum i : 1 <= i < #bowl && bowl[i] == c :: 1))
\end{verbatim}

where \texttt{validCandyType(c)\ ==\ (c\ \textasciitilde{}=\ nil)}.

\end{document}