\documentclass[11pt]{article} % standard font/input encoding \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} % graphics & color \usepackage[pdftex]{graphicx,color} % math tools \usepackage{amsmath} \usepackage{mathtools} % also loads amsmath % for nice double brackets (optional) \usepackage{stmaryrd} % source code listings \usepackage{listings} % proof trees \usepackage{ebproof} % page geometry tweaks \setlength\headheight{8pt} \setlength\headsep {20pt} \setlength\footskip {30pt} \setlength\textheight{9in} \setlength\textwidth {6.5in} \setlength\oddsidemargin {0in} \setlength\evensidemargin {0in} \setlength\topmargin {-.35in} \usepackage{url} % listings style \lstset{ basicstyle = \small\ttfamily, breaklines = true, numbers = left } % nicer epsilon \renewcommand{\epsilon}{\varepsilon} % “grammar OR” symbol \newcommand{\gor}{\;\vert\;} % keyword macro \newcommand{\kw}[1]{\ensuremath{\mathbf{#1}}} % ST roman \newcommand{\ST}{\mathrm{ST}} % angle and bracket delimiters \DeclarePairedDelimiter\angl{\langle}{\rangle} \DeclarePairedDelimiter\Brack{\llbracket}{\rrbracket} \lstdefinelanguage{cool}{ morekeywords={class,else,fi,if,in,inherits,let,loop,pool,then,while,case,esac,of,new,isvoid,true,false,self,not}, morecomment=[l]{--}, morecomment=[n]{(*}{*)}, morestring=[b]", alsoother={@}, } \lstdefinelanguage{asm}{ morekeywords={push,top,pop,swap,jump,print}, morecomment=[l]{//}, } \lstset{ language=cool, breaklines=true, keywordstyle=\bfseries, stringstyle=\ttfamily, upquote=true, emphstyle=\itshape, columns=flexible, literate={<-}{{$\gets$}}2 {<=}{{$\le$}}1, showstringspaces=false, numbers=left, numberstyle=\tiny, escapeinside={(*@}{@*)}, } \title{CS143 Spring 2024 -- Written Assignment 3} \newcommand\duedate{Tuesday, May 20, 2024 at 11:59 \textsc{pm pdt}} \begin{document} \begin{center} % Change this: \LARGE YOUR NAME -- \texttt{SUNet ID} \\ \LARGE CS143 Spring 2024 -- Written Assignment 3 \end{center} This assignment covers semantic analysis, including scoping, type systems. You may discuss this assignment with other students and work on the problems together. However, your write-up should be your own individual work, and you should indicate in your submission who you worked with, if applicable. Assignments can be submitted electronically through Gradescope as a \textsc{pdf} by \duedate. Please review the course policies for more information: \url{https://web.stanford.edu/class/cs143/policies/}. A \LaTeX{} template for writing your solutions is available on the course website. % A pdf file can be generated from this by running % pdflatex -jobname=WA3_solved WA3_template.tex % Upload WA3_solved.pdf to GradeScope % to submit the assignment! \begin{enumerate} % Problem 1 % Problem 1 \item \textbf{(16 pts)} Consider the following Cool programs: \begin{enumerate} \item \textbf{(8 pts)} \\ \begin{lstlisting} class A { x: A; -- line 2 baz(): A {{x <- new A; x;}}; -- line 3 bar(): A {new A}; -- line 4 foo(): String {"Cool!"}; }; class B inherits A { foo() : String {"are "}; }; class C inherits A { foo() : String {"Compilers "}; }; class Main { main (): Object { let io : IO <- new IO, b : B <- new B, c : C <- new C in {{ io.out_string(c.baz().foo()); io.out_string(b.baz().foo()); io.out_string(b.bar().baz().foo()); }} }; }; \end{lstlisting} What does this code currently print? By changing the types on lines 2-4 get this program to print "Compilers are Cool!". \textbf{Answer:} \newpage \item \textbf{(8 pts)} Here is an incomplete Cool program: \begin{lstlisting}[gobble=4, emph={io,x}, basicstyle=\small] class Main { main(): Object { let io: IO <- new IO, counter: Int <- 5 in { -- print 5 lines of bananas while 0 < counter loop { io.out_string("ba"); let counter: Int <- 2 in { -- print "nana" in a Cool way! while 0 < counter loop { io.out_string("na"); counter <- counter - 1; } pool; -- only print the "s" if we have more than one banana if (* INCOMPLETE *) then { io.out_string("s\n"); 1; } else 0; }; -- decrement the print counter counter <- counter - 1; } pool; }; }; }; \end{lstlisting} You need to fill the incomplete expression on line 15 so that the program prints the following output: \begin{verbatim} 5 bananas 4 bananas 3 bananas 2 bananas 1 banana \end{verbatim} Replace \lstinline!(* INCOMPLETE *)! with a single expression such that the program prints the desired output, or explain why it is not possible. \bigskip \textbf{Answer:} \end{enumerate} \newpage % Problem 2 \item \textbf{(24 pts)} Type derivations are expressed as inductive proofs in the form of trees of logical expressions. For example, the following is the type derivation for $O[Int/y] \vdash y + y: Int$: \\ \begin{center} \begin{prooftree} \Hypo[]{O[Int/y](y) = Int} \Infer1[]{O[Int/y],M,C \vdash y:Int} \Hypo[]{O[Int/y](y) = Int} \Infer1[]{O[Int/y],M,C \vdash y:Int} \Infer2[]{O[Int/y],M,C \vdash y+y:Int} \end{prooftree} \end{center} Consider the following Cool program fragment: \begin{lstlisting} class A { i: Int; j: Int; b: Bool; s: String; o: SELF_TYPE; foo(): SELF_TYPE { o }; bar(): Int { 2 * i + j - i / j - 3 * j }; }; class B inherits A { p: SELF_TYPE; baz(a: Int, b:Int): Bool { a = b }; test(c: Object): Object { (* [Placeholder C] *) }; }; \end{lstlisting} Note that the environments $O$ and $M$ at the start of the method test(...) are as follows: $$ O = \emptyset[\mbox{Int}/i][\mbox{Int}/j][\mbox{Bool}/b][\mbox{String}/s][\mbox{SELF\_TYPE}_B/o][\mbox{SELF\_TYPE}_B/p][\mbox{Object}/c][\mbox{SELF\_TYPE}_B/self]$$ $$ M = \emptyset[(\mbox{SELF\_TYPE})/(A,foo)][(\mbox{Int})/(A,bar)][(\mbox{Int,Int,Bool})/(B,baz)][(\mbox{Object})/(B,test)]$$ For each of the following expressions replacing [Placeholder C], provide the type derivation and final type of the expression, if it is well typed, otherwise explain why it isn't. Assume Cool type rules (you may omit subtyping relationships from the rules when the type is the same, e.g. $\mbox{Bool} \leq \mbox{Bool}$). \newpage \begin{enumerate} \item \textbf{(6 pts)} \begin{lstlisting} b <- p.baz(p.bar(),i) \end{lstlisting} \textbf{Answer:} \newpage \item \textbf{(6 pts)} \begin{lstlisting} p <- o.foo() \end{lstlisting} \textbf{Answer:} \newpage \item \textbf{(6 pts)} \begin{lstlisting} b <- baz(i+j,p.bar(i,o.foo())) \end{lstlisting} \textbf{Answer:} \newpage \item \textbf{(6 pts)} \begin{lstlisting} case c of s: Int => s; i: String => j; b: Object => i; esac \end{lstlisting} \textbf{Answer:} \end{enumerate} \newpage % Problem 3 \item \textbf{(16 pts)} Consider the following Cool program: \begin{lstlisting} class Main { b: B; main (): Object {{ b <- new B; b.foo(); }}; }; \end{lstlisting} Now consider the following implementations of the classes A and B. Analyze each version of the classes to determine if the resulting program will pass type checking and, if it does, whether it will execute without runtime errors. Please include a brief (1 - 2 sentences) explanation along with your answer. Note it is not sufficient to simply copy the output of the cool compiler, if it fails type checking be specific about which hypotheses cannot be satisfied for which rules. \begin{enumerate} \item \textbf{(8 pts)} \\ \begin{lstlisting} class A { i: Int <- 1; a: SELF_TYPE; foo(): Int {i}; }; class B inherits A { j: Int <- 1; baz(): Int {{i <- 2 + i; i;}}; foo(): Int {{ j <- a.baz() + a.foo(); j; }}; }; \end{lstlisting} \textbf{Answer:} \newpage \item \textbf{(8 pts)} \\ \begin{lstlisting} class A { i: Int <- 1; a: SELF_TYPE; foo(): Int {i}; }; class B inherits A{ j: Int <- 1; baz(): Int {{ i <- 2 + i; i; }}; foo(): Int { let a: A <- new B in { j <- a@B.baz() + a.foo(); j; } }; }; \end{lstlisting} \textbf{Answer:} \end{enumerate} \newpage % Problem 4 \item \textbf{(26 pts)} Consider the following extension to the Cool syntax as given on page 16 of the Cool Manual, which adds arrays to the language: \begin{equation} \begin{split} \mbox{expr} &::= \mbox{new} \ \mbox{TYPE}[\ \mbox{expr} \ ] \\ &\mid \mbox{expr}[\ \mbox{expr} \ ] \\ &\mid \mbox{expr}[\ \mbox{expr} \ ] \ <- \ \mbox{expr} \end{split} \end{equation} This adds a new type T[] for every type T in Cool, including the basic classes. Note that the entire hierarchy of array types still has Object as its topmost supertype. An array object can be initialized with an expression similar to ``my\_array:T[] $\leftarrow$ new T[n]'', where n is an Int indicating the size of the array. In the general case, any expression that evaluates to an Int can be used in place of n. Thereafter, elements in the array can be accessed as ``my\_array[i]'' and modified using a expression like ``my\_array[i] $\leftarrow$ value''. \begin{enumerate} \item \textbf{(18 pts)} Provide new typing rules for Cool which handle the typing judgments for: $O, M, C \vdash \mbox{new} \ \mbox{T}[\ e_1 \ ]$, $O, M, C \vdash e_1[\ e_2 \ ]$ and $O, M, C \vdash e_1[\ e_2 \ ] \ <- \ e_3$. Make sure your rules work with subtyping. \textbf{Answer:}\\ \newpage \item \textbf{(8 pts)} Consider the following subtyping rule for arrays: \\ \begin{center} \begin{prooftree} \Hypo[]{T_1 \leq T_2} \Infer1[]{T_1[\ ] \leq T_2[\ ]} \end{prooftree} \end{center} This rule means that $T_1[\ ] \leq T_2[\ ]$ whenever it is the case that $T_1 \leq T_2$, for any pair of types $T_1$ and $T_2$. While plausible on first sight, the rule above is incorrect, in the sense that it doesn't preserve Cool's type safety guarantees. Provide an example of a Cool program (with arrays added) which would type check when adding the above rule to Cool's existing type rules, yet lead to a type error at runtime. \textbf{Answer:}\\ \newpage \end{enumerate} % Problem 5 \item \textbf{(18 pts)} Consider another extension to the Cool language. In this case, we wish to add a special type to Cool that can either be an Int or a special value that represents ``no result''. This \textbf{MaybeInt} type will take two forms: \textbf{Some(n)} where \textbf{n} is an integer, and \textbf{Nothing}. The compiler will provide two methods: \textbf{createSomething(n:Int):MaybeInt} and \textbf{createNothing():MaybeInt} which are defined in the \textbf{Object} class and produce each of the values of the \textbf{MaybeInt} type. An example of where this type would be useful is a function like: \begin{lstlisting} divide(numerator:Int, denominator:Int):MaybeInt { if (denominator = 0) then createNothing() else createSomething(numerator / denominator) fi } \end{lstlisting} Which provides an implementation of an integer division that will not need to throw an exception when faced with a denominator of 0, but will return \textbf{Nothing} instead. To be able to use the value inside of a \textbf{MaybeInt}, we add a pattern matching statement \textbf{match} to our language. Similar to how a \textbf{switch} statement works in other languages, \textbf{match} will go to a branch depending on the form of \textbf{MaybeInt} passed to it at runtime, while also possibly introducing a new value into the scope. The value of a \textbf{match} expression is the value of the expression on the right side of the branch that was taken. Example: \begin{lstlisting} let div_result: MaybeInt in { div_result <- divide(i,j); match(div_result) { Some(n) => "The result was: ".concat(n.to_string()), Nothing => "Can't divide by zero." }; } \end{lstlisting} The grammar rule for \textbf{match} is: \begin{equation} \begin{split} \mbox{expr} &::= \mathbf{match} \ (\mbox{expr})\{\mathbf{Some(n)} => \mbox{expr}, \mathbf{Nothing} => \mbox{expr} \} \end{split} \end{equation} \begin{enumerate} \item \textbf{(6 pts)} Write a type checking rule for the \textbf{match} expression, which preserves Cool's type safety guarantees. \textbf{Answer:} \newpage \item \textbf{(12 pts)} Give the operational semantics of the \textbf{match} expression. Consider referring to the operational semantics for Let and If-True/False from the Cool manual. Assume that when looking up \textbf{MaybeInt} in the store, it will either return \textbf{Some(n)} or \textbf{Nothing}, so you may need to write two separate rules. \textbf{Answer:} \end{enumerate} \end{enumerate} \end{document}