\documentclass[letterpaper]{article}
\usepackage{fullpage,theorem,prooftree,amsmath,amssymb,url}
\usepackage{stmaryrd}
\usepackage{code}

\newcommand{\cf}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\rn}[1]{\textsc{#1}}

\newcommand{\arr}{\Rightarrow}
\newcommand{\cons}{\cf{\ ::\ }}
\newcommand{\match}{\cf{match\ }}
\newcommand{\nil}{\cf{[]}}
\newcommand{\with}{\cf{\ with\ }}
\newcommand{\xbar}{\cf{\ |\ }}
\newcommand{\removenames}{\ensuremath{\mathit{remove}}}
\newcommand{\restorenames}{\ensuremath{\mathit{restore}}}
\newcommand{\remove}{\ensuremath{\mathit{remove}}}
\newcommand{\restore}{\ensuremath{\mathit{restore}}}
\newcommand{\stype}{\ensuremath{\mathrel{\texttt{<:}}}}
\newcommand{\variant}[1]{\cf{\texttt{<} #1 \texttt{>}}}
\newcommand{\xset}[1]{\widehat{#1}}

\newcommand{\EVALONE}{\ensuremath{\longrightarrow}}

%%% Macros from Benjamin

\theoremstyle{margin}
\theorembodyfont{\rmfamily}
\newtheorem{lemma}{Lemma}
\newtheorem{exercise}{Exercise}
\newtheorem{debriefing}[exercise]{Debriefing}
\newtheorem{remarks}[exercise]{Final remarks}
\newtheorem{solution}{Solution}

\begin{document}
\begin{center}
\fbox{\large\bf CIS 500 Software Foundations}\\[5pt]
{\large\bf Homework Assignment 9}\\[5pt]

Object encodings; Featherweight Java\\[10pt]
{\bf Due:} Wednesday, December 7, 2005, by noon
\end{center}



\noindent {\bf Submission instructions:}

\medskip \noindent You must submit your solutions electronically (in ascii,
postscript, or PDF format).  Electronic solutions should be submitted
following the same instructions as last time; these can be found at
\url{http://www.seas.upenn.edu/~cis500/homework.html}.  Do {\bf not} email
your solutions to us.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\noindent\rule{\textwidth}{1pt}

The first three exercises consider an implementation of a class
representing a set of integers, in the style of TAPL Section 18.11. 
With this encoding, the type of a set of integers is:
\begin{verbatim}
Set = {
  contains : Nat -> Bool,
  add : Nat -> Unit,
  add2 : Nat -> Nat -> Unit,
  remove : Nat -> Unit
}
\end{verbatim}
This class contains a method for checking whether or not an element is in the set
(\verb'contains') and methods for adding and removing elements (\verb'add' and
\verb'remove').  The method \verb'add2' simply adds both of its arguments
to the set, naturally implemented by calling the \verb'add'
method twice.  The type for the internal representation of sets will be:
\begin{verbatim}
SetRep = {x : Ref (Nat -> Bool)}
\end{verbatim}
Following TAPL 18.11, we can implement the set class as below:
\begin{code}
setClass =
  $\lambda$r : SetRep.
    $\lambda$this : Unit -> Set.
      $\lambda$\_ : Unit.
        \{ contains = $\lambda$n:Nat. (!(r.x)) n,
          add = $\lambda$n:Nat.
            let old = (!(r.x)) in
            r.x := $\lambda$m:Nat. if m = n then true else old m,
          add2 =
            $\lambda$m:Nat. $\lambda$n:Nat.
            (this unit).add m;
            (this unit).add n,
          remove = $\lambda$n:Nat.
            let old = (!(r.x)) in
            r.x := $\lambda$m:Nat. if m = n then false else old m,
        \}
\end{code}
Finally, a function to construct a new set might look like:
\begin{code}
newEmptySet =
  $\lambda$\_ : Unit. fix (setClass \{x = ref ($\lambda$n:Nat. false)\}) unit
\end{code}

\begin{exercise}

\item Consider another definition for the constructor of an empty set:
\begin{code}
newEmptySet' = fix (setClass \{x = ref ($\lambda$n:Nat. false)\})
\end{code}
\begin{itemize}
\item Does \verb"newEmptySet'" have the same type as \verb"newEmptySet"?
\item Does \verb"newEmptySet'" have the same behavior as \verb"newEmptySet"
(think about the issue of divergence)?
\end{itemize}
\end{exercise}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{exercise}
  Now consider a subclass of \cd{Set} that has a method returning the
  size of the set.  That is, we would like an object of type:
\begin{verbatim}
SizeSet = {
  contains : Nat -> Bool,
  add : Nat -> Unit,
  add2 : Nat -> Nat -> Unit,
  remove : Nat -> Unit,
  size : Unit -> Nat
}
\end{verbatim}
\begin{itemize}
\item Define a type \verb'SizeSetRep' for the internal representation used by
this class.  (It should be a subtype of \verb'SetRep', of course.)
\item Using this representation,
write an implementation of a \verb'sizeSetClass' as a subclass of the
\verb'setClass'.  In particular, you must define the behavior of the method
\verb'add2' with inheritance.
\item Write a function to construct a new, empty \verb'SizeSet'.
\end{itemize}
\end{exercise}

\begin{solution}\
\begin{code}
SizeSetRep = \{x : Ref (Nat -> Bool), i : Ref Nat\}

sizeSetClass =
  $\lambda$r : SizeSetRep.
    $\lambda$this : Unit -> SizeSet.
      $\lambda$\_ : Unit.
        let super = setClass r this unit in
          \{ contains = super.contains,
            add =
              $\lambda$n:Nat:
                if (this unit).contains n then unit
                else
                  r.i := succ (!(r.i)); super.add n,
            add2 = super.add2,
            remove =
              $\lambda$n:Nat.
                if (this unit).contains n then
                  r.i := pred (!(r.i)); super.remove n
                else unit,
            size = $\lambda$\_:Unit. !(r.i)
          \}

newEmptySizeSet = fix (setSizeClass \{x = ref ($\lambda$n:Nat. false), i = ref 0\})
\end{code}
\end{solution}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{exercise}
Consider a subclass of \verb'Set' that adds a union operation:
\begin{verbatim}
UnionSet = {
  contains : Nat -> Bool,
  add : Nat -> Unit,
  add2 : Nat -> Nat -> Unit,
  remove : Nat -> Unit,
  union : Set -> Unit
}
\end{verbatim}
The \verb'union' operation will update the object by adding all of the
elements in the set given as an argument.  Are there any problems in
implementing an object of this type (with the desired behavior for
\verb'union')?  You may assume that the internal representation could be
entirely changed and that the language contains other data structures such as
list and trees.  Are there any problems implementing such an object in Java?
\end{exercise}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\noindent\rule{\textwidth}{1pt}

\noindent The following four exercises are based on an extension of
Featherweight Java with exceptions (TAPL 19.4.4).  They build upon each
other.

\begin{exercise}
Extend the syntax of Featherweight Java with \cf{throw} and \cf{try} forms.

\[
\begin{array}{rcll}
   \cf{t} &::=& \ldots & \quad \mbox{terms:} \\
          &   & \cf{throw\ t} & \quad \mbox{throw an exception} \\
          &   & \cf{try\ t\ \overline{cl}} & \quad \mbox{handle exceptions}
   \\
   \\
   \cf{cl} &::=& \cf{catch\ (C\ x)\ t} & \quad \mbox{exception handler}
\end{array}
\]

\noindent Some of the new operational semantics are:

\begin{itemize}

\item If the thrown exception is a subtype of the first clause in the
exception handler, that code is executed.

\[
   \prooftree
      \cf{D \stype C}
      \justifies
      \cf{try\ (throw\ new\ D(\overline{v}))\
          (catch\ (C\ x)\ t)\ \overline{cl}
          \longrightarrow
          [x \mapsto new\ D(\overline{v})]t
      }
      \using \rn{E-Catch}
   \endprooftree
\]

\item If the exception is the wrong type for the first handler,
check the rest of the handlers.

\[
   \prooftree
      \cf{D \not\stype C}
      \justifies
      \cf{try\ (throw\ new\ D(\overline{v}))\
          (catch\ (C\ x)\ t)\ \overline{cl}
          \longrightarrow
          try\ (throw\ new\ D(\overline{v}))\
          \overline{cl}
      }
      \using \rn{E-Next}
   \endprooftree
\]

\item If there are no handlers left, the exception continues to propagate.

\[
   \prooftree
      \justifies
      \cf{try\ (throw\ v) \longrightarrow throw\ v}
      \using \rn{E-Throw-Try}
   \endprooftree
\]

\item For method calls, if we throw an exception while evaluating the
receiver of a method invocation, we propagate it.

\[
   \prooftree
      \justifies
      \cf{(throw\ v).m(\overline{t}) \longrightarrow throw\ v}
      \using \rn{E-Throw-Recv}
   \endprooftree
\]

\item If we throw an exception while evaluating one of the arguments of a
method call, we propagate it.

\[
   \prooftree
      \justifies
         \cf{v_0.m(\overline{v}, throw\ v, \overline{t})
             \longrightarrow
             throw\ v}
      \using \rn{E-Throw-Arg}
   \endprooftree
\]

\end{itemize}

\noindent \textbf{\textit{Question:}} What other rules should we add to the
operational semantics?

\end{exercise}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Another feature of Java is that method types keep track of what exceptions
could be thrown during evaluation of that method. We'll do the something
similar here by adding a \cf{throws} clause to method declarations.  Thus,
we have:

\[
\begin{array}{rcll}
\cf{M} &::=&
\cf{C\ m(\overline{C}\ \overline{x})\ throws\ \xset{E}\ \{\ return\ t;\
\}} & \quad \mbox{method declaration}
\end{array}
\]

\noindent Here, \cf{\xset{E}} denotes a \emph{set} of class names; this is
in contrast to \cf{\overline{E}} which denotes a list (or sequence) of class
names.  Many other things in Featherweight Java need to be modified in order
to accommodate this change.

\begin{itemize}

\item To make sure that this \cf{throws} declaration is correct, the typing
judgment must also calculate the set of exceptions that \emph{might} be
thrown when a term is evaluated.  Thus, they now take the following form:

\[
   \Gamma \vdash \cf{t} : \cf{D\ throws\ \xset{E}}
\]

\noindent When \cf{\xset{E}} is empty, we abbreviate this judgment to
$\Gamma \vdash \cf{t} : \cf{D}$.  In general, we'll calculate \cf{\xset{E}}
in a conservative manner; that is, \cf{\xset{E}} may sometimes contain types
(i.e., class names) that \cf{t} cannot possibly throw or it may contain
``redundant'' class names.

\item We ``know'' that a \cf{throw} expression will throw an exception of
type \cf{C}.  Like \cf{raise} in Chapter 14, the \cf{throw} expression
itself can have any type.

\[
   \prooftree
   \Gamma \vdash \cf{t} : \cf{C\ throws\ \xset{E}}
   \justifies
   \Gamma \vdash \cf{throw\ t} : \cf{D\ throws\ \{C\} \cup \xset{E}}
   \using \rn{T-Throw}
   \endprooftree
\]

\noindent Note that this rule conservatively calculates the set of
exceptions that can be thrown by an expression.  For example, the following
derivation is valid, assuming \cf{A} is a class with a zero-argument
constructor.

\[
   \prooftree
   \prooftree
      \prooftree
      \justifies
      \Gamma \vdash \cf{new\ A()} : \cf{A}
      \using \rn{T-New}
      \endprooftree
   \justifies
   \Gamma \vdash \cf{throw\ new\ A()} : \cf{B\ throws\ \{A\}}
   \using \rn{T-Throw}
   \endprooftree
   \justifies
   \Gamma \vdash
      \cf{throw\ (throw\ new\ A())}
      : \cf{C\ throws\ \{A,B\}}
   \using \rn{T-Throw}
   \endprooftree
\]

\noindent However, it's clear that \cf{throw\ (throw\ new\ A())} throws only
an exception of type \cf{A}.

\item In a \cf{try} expression, we need to figure out what sorts of
exceptions could be thrown in the ``body'' and what sorts can be handled by
the exception handlers.

\[
   \prooftree
   \Gamma \vdash \cf{t} : \cf{A_0\ throws\ \xset{C}}
   \quad\quad\quad
   \Gamma \vdash \cf{\overline{cl}} :
      \cf{A\ throws\ {\xset{D}}\ handles\
      \xset{E}}
   \quad\quad
   \cf{A_0 \stype A}
   \quad\quad
%   \cf{\overline{A} \stype A}
   \justifies
   \Gamma \vdash
      \cf{try\ t\ \overline{cl}} :
      \cf{A\ throws\ (\xset{C} - \xset{E}) \cup
      \xset{D}}
   \using \rn{T-Try}
   \endprooftree
\]

\noindent Note that 
%$\Gamma \vdash
%\cf{\overline{cl}} : \cf{\overline{A}\ throws\ \overline{\xset{D}}\ handles\
%\overline{E}}$ is shorthand for $\Gamma \vdash \cf{cl_1} : \cf{A_1\
%throws\ \xset{D_1}\ handles\ E_1}$, \ldots, $\Gamma \vdash \cf{cl_n} :
%\cf{A_n\ throws\ \xset{D_n}\ handles\ E_n}$, and
 \cf{\xset{C}- \xset{E}} is defined as $$\{ \cf{A} \in \cf{\xset{C}} \,\,|\,\,
\cf{A} \text{ is not a subtype of any type in }
\cf{\{E_1,\ldots,E_n\}} \} \, .$$

\noindent This rule relies on a new judgment that type checks the \cf{catch}
clauses of a \cf{try} expression.  This judgment, which takes the form
   $\Gamma \vdash
   \cf{\overline{cl}} :
   \cf{A\ throws\ \xset{D}\ handles\
   \xset{E}}$,
determines the type of each exception handling clause, the set of exceptions
that could be thrown when evaluating the handler, and the
exceptions that the clauses handle. 
We define this judgment with the single rule:

   \[
      \prooftree
      \begin{array}{c}
%      \mbox{for each } \cf{(catch\ (C_i\ x) t_i)} \in \cf{\overline{cl}} \quad
      \Gamma, \cf{x}:\cf{\overline{C}} \vdash
         \cf{\overline{t}} : \cf{\overline{A}\ throws\ \overline{\xset{B}}}
      \\
      \cf{A_i} <: \cf{A}  \quad
      \xset{\cf{B}} = \bigcup \cf{\xset{B_i}} \quad
      \xset{\cf{C}} = \bigcup \{\cf{C_i}\}
      \end{array}
      \justifies
      \Gamma \vdash
         \cf{\overline{catch\ (C\ x)\ t}}
         :
         \cf{A\ throws\ \xset{B}\
             handles\ \xset{C}}
      \using \rn{T-Handler}
      \endprooftree
   \]

\noindent Note that $\Gamma \vdash \cf{\overline{t}} : \cf{\overline{A}\
throws\ \overline{\xset{B}}}$ is short-hand for $\Gamma \vdash \cf{t_1} :
\cf{A_1\ throws\ \xset{B_1}}$, $\Gamma \vdash \cf{t_2} : \cf{A_2\ throws\
\xset{B_2}}$, \ldots, $\Gamma \vdash \cf{t_n} : \cf{A_n\ throws\
\xset{B_n}}$.


 For example, the following
should be derivable (note again that our analysis is conservative here):
\begin{itemize}

   \item $\Gamma \vdash
      \cf{try\ (throw\ new\ A())\
               (catch\ (A\ x)\ (throw\ new\ A()))} :
      \cf{C\ throws\ \{A\}}$

   \item $\Gamma \vdash
      \cf{try\ (throw\ new\ A())\
               (catch\ (B\ x)\ (throw\ new\ C()))} :
      \cf{D\ throws\ \{A,C\}}$ when \cf{A \not\stype B}.

   \item $\Gamma \vdash
      \cf{try\ (throw\ new\ A())\
               (catch\ (B\ x)\ (throw\ new\ C()))} :
      \cf{D\ throws\ \{C\}}$ when \cf{A \stype B}.

\end{itemize}

\item Now consider type checking a method call. The exceptions that could be
thrown in this case include those that could be thrown when computing the
receiver of the method invocation, computing the arguments, or executing the
actual method call.

\[
   \prooftree
      \begin{array}{ll}
      \Gamma \vdash \cf{t_0} :
         \cf{C_0\ throws\ \xset{A}}
      &
      \mathit{mtype}(\cf{m}, \cf{C_0}) =
      \cf{\overline{D} \to C\ throws\ \xset{E}}
      \\
      \Gamma \vdash \cf{\overline{t}} :
      \cf{\overline{C}\ throws\ \overline{\xset{B}}}
      &
      \cf{\overline{C} \stype \overline{D}}
      \end{array}
      \justifies
      \Gamma \vdash \cf{t_0.m(\overline{t})} :
      \cf{C\ throws\ \xset{E} \cup \xset{A} \cup \bigcup \xset{B_i}}
      \using \rn{T-Invk}
   \endprooftree
\]

\noindent This is where the \cf{throws} annotation on method declarations
comes in.  We must modify $\mathit{mtype}$ so that it returns this set, as
in:

\[
   \mathit{mtype}(\cf{m},\cf{C_0}) =
   \cf{\overline{D} \to C\ throws\ \xset{E}}
\]


\item We also have to modify the definitions of $\mathit{mbody}$ and
$\mathit{override}$. For example, the rules for $\mathit{mbody}$ become:

   \[
      \prooftree
         \begin{array}{c}
            \mathit{CT}(\cf{C}) =
            \cf{class\ C\ extends\ D\
            \{\overline{C}\ \overline{f}; K\ \overline{M}\}}
            \\
            \cf{m} \text{ is not defined in } \cf{\overline{M}}
         \end{array}
         \justifies
         \mathit{mbody}(\cf{m}, \cf{C}) =
         \mathit{mbody}(\cf{m}, \cf{D})
      \endprooftree
   \]

   \[
      \prooftree
         \begin{array}{c}
            \mathit{CT}(\cf{C}) =
            \cf{class\ C\ extends\ D\
            \{\overline{C}\ \overline{f}; K\ \overline{M}\}}
            \\
            \cf{B\ m(\overline{B}\ \overline{x})\
            throws\ \xset{E}\ \{ return\ t; \}}
            \in
            \cf{\overline{M}}
         \end{array}
         \justifies
         \mathit{mbody}(\cf{m}, \cf{C}) =
         (\cf{\overline{x}}, \cf{t})
      \endprooftree
   \]



\item We need to modify the rule for type-checking methods in order to take
into account \cf{throws} clauses.

\[
   \prooftree
      \begin{array}{c}
         \cf{\overline{x}:\overline{C}, this:C \vdash t_0 : E_0\ throws\
         \xset{A}}
         \\
         \cf{E_0 \stype C_0}
         \\
         \mathit{CT}(\cf{C}) =
         \cf{class\ C\ extends\ D\ \{\ldots\}}
         \\
         \mathit{override}(\cf{m}, \cf{D}, \cf{\overline{C} \to C_0\
         throws\ \xset{E}})
         \\
         \text{each type in } \cf{\xset{A}}
         \text{ is a subtype of some type in } \cf{\xset{E}}
      \end{array}
   \justifies
      \cf{C_0\ m(\overline{C}\ \overline{x})\ throws\ \xset{E}\
          \{ return\ t_0; \}\ OK\ in\ C}
   \endprooftree
\]
\end{itemize}

\medskip \noindent \textit{\textbf{Some questions now:}}

\begin{enumerate}

\item What are the rule(s) for defining $\mathit{mtype}$?

\item What are the rule(s) for defining $\mathit{override}$? 

%\item How should we typecheck exception handlers \cf{cl}?  In
%otherwords, what rule(s) do we need to derive
%\[
%   \Gamma \vdash
%   \cf{cl} :
%   \cf{A\ throws\ \xset{D}\ handles\ E} \, \, \, ?
%\]

\item How should we state the rules \rn{T-Var}, \rn{T-Field}, \rn{T-New},
\rn{T-UCast}, \rn{T-DCast}, and \rn{T-SCast} so that they also calculate the
set of exceptions that could be thrown?  (While we introduce
\texttt{ClassCastEx\-cep\-tion} in a later exercise, you do \emph{not} need
to worry about it here since none of our evaluation rules mention it yet.)


\end{enumerate}

\end{exercise}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Prove the preservation lemma for this extension by induction on the given
typing derivation.  The preservation lemma states:

\begin{quote} If $\Gamma \vdash \cf{t} : \cf{C\ throws\ \xset{E}}$ and
$\cf{t \longrightarrow t'}$ then $\Gamma \vdash \cf{t'} : \cf{D\ throws\ \xset{F}}$ 
where $\cf{D \stype C}$ and each class in \cf{\xset{F}} is a
subtype of some class in \cf{\xset{E}}. \end{quote}


\noindent You only need to show the cases for \rn{T-Try} and \rn{T-Invk}.
You may use the following lemmas without proof: \begin{itemize}

   \item If $\mathit{fields}(\cf{D}) = \cf{\overline{D}\
   \overline{f}}$ and \cf{C \stype D}, then $\mathit{fields}(\cf{C}) =
   \cf{\overline{D}\ \overline{f},\overline{C}\ \overline{g}}$ for some
   \cf{\overline{C}} and \cf{\overline{g}}.

   \item If $\Gamma \vdash \cf{v} : \cf{C\ throws\ \xset{E}}$, then
   $\cf{\xset{E}} = \emptyset$.

   \item If $\Gamma, \cf{\overline{x}}:\cf{\overline{B}} \vdash \cf{t} :
   \cf{D\ throws\ \xset{E}}$ and $\Gamma \vdash \cf{\overline{v}}:
   \cf{\overline{A}}$ where \cf{\overline{A} \stype \overline{B}}, then
   $\Gamma \vdash [\cf{\overline{x}} \mapsto \cf{\overline{v}}]
   \cf{t} : \cf{C\ throws\ \xset{E'}}$ for some \cf{C \stype D} and where
   each type in \cf{\xset{E'}} is a subtype of some type in \cf{\xset{E}}.
   (Note that we're substituting in \emph{values} here!)

   \item Any inversion lemmas or canonical forms lemmas (make sure to at
   least state the ones you use, though).

\end{itemize}

\end{exercise}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Suppose we add the following evaluation rule
\[
   \prooftree
   \cf{C \not\stype D}
   \justifies
   \cf{(D)(new\ C(\overline{v})) \longrightarrow
      throw\ new\ ClassCastException()}
   \endprooftree
\]
where \cf{ClassCastException} is a class with no fields or methods, and a
zero argument constructor.  How should we state the progress lemma now?
Keep in mind that we haven't changed any typing rules from previous
exercises.

\end{exercise}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\noindent\rule{\textwidth}{1pt}

\begin{exercise}  Why does Java separate \cf{RuntimeException}s from other
\cf{Exception}s?  Note that \texttt{RuntimeEx\-cep\-tion}s are exempt from
compile-time checks: they do not need to appear in the \cf{throws} clause of
a method declaration, nor do they need to be handled by a \cf{catch} clause.
This is not the case for other \cf{Exception}s.  \end{exercise}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{debriefing}\
\begin{enumerate}
\item How many hours did each person in your group spend on this assignment,
including time taken to read TAPL?
\item Would you rate it as easy, moderate, or difficult?
\item Did everyone in your study group participate?
\item How deeply do you feel you understand the material it covers
(0\%--100\%)?
\end{enumerate}
If you have any other comments, we would like to hear them; please
send them to {\tt cis500@cis.upenn.edu}.
\end{debriefing}



\end{document}
