\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{textcomp,lmodern,fixcmex}
\usepackage[margin=1in]{geometry}
\usepackage{mathtools}
\usepackage{makebox}
\usepackage{listings}
\usepackage{enumitem}
\usepackage{ebproof}
\usepackage{calc}
\usepackage[pdfusetitle]{hyperref}

\renewcommand{\epsilon}{\varepsilon}
\newcommand{\gor}{\mathrel{\makebox*{$\to$}{$|$}}}
\newcommand{\kw}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\param}[1]{\ensuremath{\mathit{#1}}}

\DeclarePairedDelimiter\angl{\langle}{\rangle}
\DeclarePairedDelimiter\Brack{\text{\textlbrackdbl}}{\text{\textrbrackdbl}}

\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,read,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 2026 -- Written Assignment 3}
\newcommand\duedate{Tuesday, May 19, 2026 at 11:59 \textsc{pm pdt}}

\begin{document}
\begin{center}
% Change this:
\LARGE CS143 Spring 2026 -- Written Assignment 3
\end{center}

This assignment covers semantic analysis, including scoping, type systems,
and code generation. 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.

\begin{enumerate}
% Problem 1
\item The Un-Cool Society tore up a precious scroll containing the first-ever Cool program!
Thankfully, most of the the code was able to be pieced together:
\begin{enumerate}
    \item ~
    \begin{lstlisting}[gobble=4, emph={x,io,a,b,c}, basicstyle=\small]
    class A {
        x: A;
        one(): A { x <- (* ??? BLANK 1 ??? *) };
        two(): A { x };
        string(): String { (* ??? BLANK 2 ??? *) };
    };
    class B inherits A {
        string(): String { (* ??? BLANK 3 ??? *) };
    };
    class C inherits A {
        init(): A { x <- new A };
        three(): A { new B };
        string(): String { (* ??? BLANK 4 ??? *) };
    };
    class Main {
        main(): Object {
            let io: IO <- new IO,
                c : C  <- new C
            in {
                c.init();
                io.out_string(c.three().one().string());
                io.out_string(" ");
                io.out_string(c.two().one().string());
                io.out_string(" ");
                io.out_string(c.one().string());
                io.out_string(" ");
                io.out_string(c.three().string());
            }
        };
    };
    \end{lstlisting}

    \newpage

    Replace \textit{only} blanks 1-4 on lines 3, 5, 8, and 13 respectively with
    \textbf{a single expression each (no blocks)} so that the code
    prints out \texttt{``Cool compilers are Cool''}.

    \bigskip

    \textbf{Answer:}

    \newpage

    \item Here is another incomplete COOL program that was recovered, that a COOL developer is trying to complete :
    \begin{lstlisting}[gobble=4, emph={io,x}, basicstyle=\small]
    
class Main {
      main(): Object {
        let io : IO <- new IO, n : Int <- 5, c : Int <- n in
          while 0 < c loop {
            io.out_int(c);
            io.out_string(" ");
            io.out_string("C-");
            let n : Int <- (* YOUR CODE HERE *), c : Int <- 0 in
              while c < n loop {
                io.out_string("OO-");
                c <- c + 1;
              } pool;
            io.out_string("L\n");
            c <- c - 1;
          } pool
      };
    };
    \end{lstlisting}

    The developer does not understand  scoping in COOL and needs your help with filling in the incomplete expression on line 9 so that the
    program prints the following output:
    \begin{verbatim}
5 C-OO-L
4 C-OO-OO-L
3 C-OO-OO-OO-L
2 C-OO-OO-OO-OO-L
1 C-OO-OO-OO-OO-OO-L
    \end{verbatim}
    Replace \lstinline!(* YOUR CODE HERE *)! 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 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[\mathrm{Int}/y], M, C \vdash y + y: \mathrm{Int}$:
\begin{center}
\begin{prooftree}
    \hypo[]{O[\mathrm{Int}/y](y) = \mathrm{Int}}
    \infer1[[Var]]{O[\mathrm{Int}/y],M,C \vdash y: \mathrm{Int}}
    \hypo[]{O[\mathrm{Int}/y](y) = \mathrm{Int}}
    \infer1[[Var]]{O[\mathrm{Int}/y],M,C \vdash y:\mathrm{Int}}
    \infer2[[Arith]]{O[\mathrm{Int}/y],M,C \vdash y+y:\mathrm{Int}}
\end{prooftree}
\end{center}
The [Var] and [Arith] labels refer to the corresponding inference rules in the Cool Reference Manual, section 12.2.\footnote{See \url{https://web.stanford.edu/class/cs143/materials/cool-manual.pdf}, pp.\ 18--22.}

\smallskip

Consider the following Cool program fragment:
\begin{lstlisting}[emph={i,b,s,o,a,x,y}, basicstyle=\small]
class A {
    i: Int;
    b: Bool;
    s: String;
    o: SELF_TYPE;
    foo(): SELF_TYPE { o };
    bar(): Int { 2 * i + 1 };
};

class B inherits A {
    a: A;
    baz(x: Int, y: Int): Bool { x = y };
    test(): Object { (* PLACEHOLDER *) };
};
\end{lstlisting}
Note that the environments $O$ and $M$ at the start of the method test() are as follows:
\begin{gather*}
    O = \emptyset[\mathrm{Int}/i][\mathrm{Bool}/b][\mathrm{String}/s][\mathrm{SELF\_TYPE}_{\mathrm{B}}/o][\mathrm{A}/a][\mathrm{SELF\_TYPE}_{\mathrm{B}}/\mathit{self}], \\[2ex]
    \begin{aligned}
    M = \emptyset&[(\mathrm{SELF\_TYPE})/(\mathrm{A},\mathrm{foo})][(\mathrm{Int})/(\mathrm{A},\mathrm{bar})] \\
                 &[(\mathrm{SELF\_TYPE})/(\mathrm{B},\mathrm{foo})][(\mathrm{Int})/(\mathrm{B},\mathrm{bar})] \\
                 &[(\mathrm{Int,Int,Bool})/(\mathrm{B},\mathrm{baz})][(\mathrm{Object})/(\mathrm{B},\mathrm{test})].
    \end{aligned}
\end{gather*}

For each of the following expressions replacing \lstinline{(* PLACEHOLDER *)}, provide the inferred type of the expression, as well as its derivation as a proof tree.\footnote{To draw proof trees in \LaTeX, consider using the \href{https://ctan.org/pkg/ebproof?lang=en}{\textsf{ebproof}} package. You can also use the tree in the template as an example.} For brevity, you may omit subtyping relations where the same type is on both sides (e.g., $\mathrm{Bool} \le \mathrm{Bool}$). You also do not need to label each step with the inference rule name like we did above.

\newpage

\newcommand{\Str}{\mathrm{String}}
\newcommand{\Bool}{\mathrm{Bool}}
\newcommand{\Int}{\mathrm{Int}}
\newcommand{\A}{\mathrm{A}}
\newcommand{\B}{\mathrm{B}}
\newcommand{\ST}{\mathrm{SELF\_TYPE}}

\begin{enumerate}
    \item \lstinline[keepspaces=true, emph={s,b,i}]|b <- self.baz(i, 1);|

        \textbf{Answer}:
        \vspace{6cm}

    \item \lstinline[keepspaces=true, emph={c}]{let c: A <- self.foo() in c.foo()}

        \textbf{Answer}:
        \vspace{6cm}

    \item \lstinline[keepspaces=true, emph={a,i}]{if 1 <= i then self.foo() else a.foo() fi}

        \textbf{Answer}:
\end{enumerate}

\newpage

% Problem 3
\item Consider the following Cool program:
\begin{lstlisting}[emph={b}, basicstyle=\small]
class Main {
    b: B;
    main(): Object {{
        b <- new B;
        b.set().baz();
    }};
};
\end{lstlisting}
Now consider the following implementations of the classes A and B. Analyze each version of the classes to determine:
\begin{itemize}
    \item if the resulting program will pass type checking
    \item if it does, whether it will execute without runtime errors
\end{itemize}
Please include a brief (1--2 sentences) explanation along with your answer.  Note it is not sufficient to simply copy the output of the reference Cool compiler: if it fails type checking, you must specify which hypotheses cannot be satisfied for which rules.

\begin{enumerate}
    \item ~\\
    \begin{lstlisting}[gobble=4, emph={i,j,a}, basicstyle=\small]
    class A {
        a_str: String <- "Cool";
        a: SELF_TYPE;
        set(): SELF_TYPE {{ a <- new A; }};
        foo(): String {a_str};
    };

    class B inherits A {
        b_str: String <- "Language";
        foo(): String { a_str.concat(b_str)};
        baz(): String {
            foo().concat(a@A.foo())
        };
    };
    \end{lstlisting}
    \textbf{Answer:}
     \vspace{6cm}

    \item ~\\
    \begin{lstlisting}[gobble=4, emph={i,j,a}, basicstyle=\small]
    class A {
        a_str: String <- "Cool";
        a: A;
        set(): A {{ a <- new A; }};
        foo(): String {a_str};
    };

    class B inherits A {
        b_str: String <- "Language";
        foo(): String { a_str.concat(b_str)};
        baz(): String {
            foo().concat(a@A.foo())
        };
    };
    \end{lstlisting}
    \textbf{Answer:}
     \vspace{6cm}
     
    \item ~\\
    \begin{lstlisting}[gobble=4, emph={i,j,a}, basicstyle=\small]
    class A {
        a_str: String <- "Cool";
        a: A;
        set(): SELF_TYPE {{ a <- new SELF_TYPE; }};
        foo(): String {a_str};
    };

    class B inherits A {
        b_str: String <- "Language";
        foo(): String { a_str.concat(b_str)};
        baz(): String {
            foo().concat(a@A.foo())
        };
    };
    \end{lstlisting}
    \textbf{Answer:}
     \vspace{6cm}
     
    \item ~\\
    \begin{lstlisting}[gobble=4, emph={i,j,a}, basicstyle=\small]
    class A {
        a_str: String <- "Cool";
        a: A;
        set(): SELF_TYPE {{ a <- new SELF_TYPE; self;}};
        foo(): String {a_str};
    };

    class B inherits A {
        b_str: String <- "Language";
        foo(): String { a_str.concat(b_str)};
        baz(): String {
            foo().concat(a@A.foo())
        };
    };
    \end{lstlisting}
    \textbf{Answer:}
     \vspace{6cm}

     
\end{enumerate}

\newpage

% Problem 4
\item Consider the following extensions to Cool:
\begin{enumerate}

    \item Tuples.
    \begin{align*}
        \mathit{expr} &\Coloneqq \ldots \\
                      &\gor \kw{new}\ \angl{\ \mathrm{TYPE}\ \Brack{, \mathrm{TYPE}}^*\ }\ [\ \mathit{expr}\ \Brack{, \mathit{expr}}^* \ ] \\
                      &\gor \mathit{expr}\ [\ \mathrm{INT} \ ]
    \end{align*}

    A tuple is a fixed-size list of values of potentially different types. Empty tuples are not allowed. We define a new family of types called \emph{tuple types} $\angl{T_1, T_2, \ldots, T_n}$, where $T_1, T_2, \ldots, T_n$ could be any type in Cool (including SELF\_TYPE and other tuple types). Note that the entire hierarchy of tuple types still has Object as its topmost supertype. Additionally, the subtype relation between tuple types is defined as follows:
    \[
        \angl{T_1, T_2, \ldots, T_n} \le \angl{T'_1, T'_2, \ldots, T'_n} \quad \text{if and only if } T_i \le T'_i \text{ for all $i$}.
    \]

    A tuple object can be initialized with an expression similar to
    \[my\_tuple\colon \angl{\mathrm{Int},\mathrm{Object}} \gets \kw{new}\ \angl{\mathrm{Int},\mathrm{String}} [42, \mathtt{``answer"}];\]
    Thereafter, the $i$\textsuperscript{th} element in the tuple can be accessed as ``$\mathit{my\_tuple}[i]$''. Tuple elements are 0-indexed. The tuple index is an integer literal that is always known at compile time.

    \smallskip

    Provide new typing rules for Cool which handle the typing judgments for the two new forms of expressions.
    As an example, your type rules should ensure the following given the earlier declaration:
    \[
        O, M, C \vdash \mathit{my\_tuple}[0] : \mathrm{Int} \qquad\qquad
        O, M, C \vdash \mathit{my\_tuple}[1] : \mathrm{Object}
    \]

    \emph{Hint: See [New] in the Cool manual for an example that deals with SELF\_TYPE in a way similar to how you will have to.}

    \bigskip

    \bigskip

    \begin{minipage}{\textwidth}
    \textbf{Answer:}
    \vspace{7cm}
    \end{minipage}
    \newpage
    
    \item Permissive method overriding.

    In Cool a subtype can only override a method with a method with exactly the same formal parameters and return type. The rules can also be written formally as the following typing judgements (using slightly informal notation to quantify over the elements in environments):
    \begin{center}
    \begin{prooftree}
        \hypo{T_i = S_i \quad \forall i \in \{1, \ldots, n+1\}}
        \infer1[Method Subtype]{(T_1, \ldots, T_n, T_{n+1}) \leq (S_1, \ldots, S_n, S_{n+1})}
    \end{prooftree}
    \end{center} \smallskip
    \begin{center}
    \begin{prooftree}
        \hypo{T_c = T_p \quad \lor \quad (T_c ~ \kw{inherits} ~ T_p' \land T_p' \leq T_p)}
        \infer[no rule]1{M \vdash \forall m \in M(T_p)\colon M(T_c, m) \leq M(T_p, m)}
        \infer1[Class Subtype]{M \vdash T_c \leq T_p}
    \end{prooftree}
    \end{center}

    The Method Subtype rule says that if a class $X$ has a method $f$ and class $Y$ has a method $g$, to establish that $f$ conforms to $g$ (i.e., $M(X, f) \leq M(Y, g)$), we must show $M(X, f) = (T_1, ..., T_n, T_{n+1}) = (S_1, ..., S_n, S_{n+1}) = M(Y, g)$.

    The Class Subtype rules says that for a class $T_c$ to be considered a subtype of a class $T_p$ we must establish two things:
    \begin{itemize}
        \item $T_c$ must either be equal to $T_p$ or it must inherit from some class $T_p'$ where $T_p'$ is a subtype of $T_p$.
        \item And for every method $m$ on $T_p$, $T_c$ must also have a method $m$ such that the types of the methods are conforming (as defined by the Method Subtype rule). I.e., $M(T_c, m) \le M(T_p, m)$.
    \end{itemize}
    Note in Cool that we consider it an error for $T_c$ to inherit from $T_p$ but fail the second test.

    The Method Subtype rule is more restrictive than necessary to ensure type safety.  Rewrite it with new hypotheses so that $T_i$ need not equal $S_i$.  Note your solution should still ensure type safety without changing the rules for dispatch. Specifically, given $C \le P$ with a method $m$ if
    \[
        \mathit{out} \gets (p\mathpunct{:} P).m(e_1, e_2, \ldots, e_n);
    \]
    type checks then so should
    \[
        \mathit{out} \gets (c\mathpunct{:} C).m(e_1, e_2, \ldots, e_n);
    \]
    for the same arguments and output variable.


    \bigskip

    \textbf{Answer:}

\end{enumerate}

\newpage

% Problem 5
\item Consider the following assembly language used to program a stack ($r$, $r_1$, and $r_2$ denote arbitrary registers):
    \begin{itemize}
        \item $\kw{push}\ \param{offset}\  r$: copies the value of $r$ and pushes it onto the stack with a provided offset. An offset of 0 pushes a value to the top of the stack, an offset of 1 pushes a value to the second-highest position in the stack, etc.
        \item $\kw{read}\ \param{offset}\ r$: copies the value at the provided offset from the top of the stack into $r$. This command does not modify the stack. An offset of 0 reads the value at the top of the stack, an offset of 1 reads the value at the second-from-top of the stack, etc.
        \item $\kw{pop}\ \param{offset}$: discards the value at the provided offset from the top of the stack. An offset of 0 pops the value at the top of the stack, an offset of 1 pops the value at the second-highest position in the stack, etc.
        \item $r_1 \mathbin{{*}{=}} r_2$: multiplies $r_1$ and $r_2$ and saves the result in $r_1$. $r_1$ may be the same as $r_2$.
        \item $r_1 \mathbin{{/}{=}} r_2$: divides $r_1$ with $r_2$ and saves the result in $r_1$. $r_1$ may be the same as $r_2$. Remainders are discarded (e.g., $5 / 2 = 2$).
        \item $r_1 \mathbin{{+}{=}} r_2$: adds $r_1$ and $r_2$ and saves the result in $r_1$. $r_1$ may be the same as $r_2$.
        \item $r_1 \mathbin{{-}{=}} r_2$: subtracts $r_2$ from $r_1$ and saves the result in $r_1$. $r_1$ may be the same as $r_2$.
        \item $\kw{jump}\ r$: jumps to the line number in $r$ and resumes execution.
        \item $\kw{print}\ r$: prints the value in $r$ to the console.
    \end{itemize}
The machine has two registers available to the program: \textbf{reg1}, and \textbf{reg2}. The stack is permitted to grow to a finite, but very large, size. If an invalid line number is invoked, a number is divided by zero, \kw{push}, \kw{read}, or \kw{pop} is executed with an invalid offset, or the maximum stack size is exceeded, the machine crashes.

\bigskip

Write code to enumerate and print the factorials ($F_n = n \times F_{n-1}$ where $F_1 = 1$; e.g., $1, 2, 6, 24, \ldots$) starting at $F_1$. Assume that the code will be placed at line 100, and will be invoked by pushing 1, 1 onto the stack $\angl{\$, \ldots, 1, 1}$, storing 100 in \lstinline[language=asm]{reg1}, and running \lstinline[language=asm]{jump reg1}.

Your code should use the \kw{print} opcode to display numbers in the sequence. You may not hardcode constants nor use any other instructions besides the ones given above. There is no need to keep the number in memory after it has been printed out.  Your code should not terminate (or crash) after any amount of time.  Assume that registers and the stack can hold arbitrarily large integers so computation will never overflow.

Hint: it may help to comment each line with a symbolic machine state and think about what the state the code should be in at the end.
(You are not required to do this but it will help us give you partial credit if you do.)
E.g.:

\begin{lstlisting}[language=asm, mathescape, numbers=none]
// initial:  reg1=$100$   reg2=        stack=$\angl{n, F_{n-1}}$
\end{lstlisting}
\begin{lstlisting}[language=asm, mathescape, firstnumber=100]
read 0 reg2 // reg1=$100$   reg2=$F_{n-1}$   stack=$\angl{n, F_{n-1}}$
pop 0       // reg1=$100$   reg2=$F_{n-1}$   stack=$\angl{n }$
...
\end{lstlisting}
\begin{lstlisting}[language=asm, mathescape, numbers=none]
// final:    ???
\end{lstlisting}

\newpage

\textbf{Answer:}


\bigskip

    
\end{enumerate}
\end{document}