\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}