\documentstyle[]{article}
\setlength{\textheight}{8.625in}
\setlength{\topmargin}{-1cm}
\setlength{\oddsidemargin}{0.25in}
\setlength{\textwidth}{6in}
\newcommand{\prg}[1]{\tt\verb@#1@}
\newcommand{\noi}{\noindent}
\newcommand{\pni}{\par \skp{1} \noi}
\newcommand{\skp}[1]{\vspace{#1\baselineskip}}
\newcommand{\Cl}[2]{\mbox{Clos}_{#1}(#2)}
\newcommand{\npar}{\par \skp{1}}
\newcommand{\QED}%
      {\begin{quote}
       \raggedleft $\Box$
       \end{quote}
      }
\newcommand{\lbrac}{[\![}
\newcommand{\rbrac}{]\!]}
\newcommand{\Nat}{\mbox{\hspace{0.2em}N\hspace{-0.9em}I\hspace{0.5em}}}
\newcommand{\Pow}{\mbox{\hspace{0.2em}P\hspace{-0.9em}I\hspace{0.5em}}}
\newcommand{\Boole}{\mbox{%
                     \hspace{0.2em}B\hspace{-0.9em}I\hspace{0.5em}}}
\newcommand{\TPU}[3]{\mbox{{\bf T}}_{#1}\uparrow #2(#3)}
\newcommand{\TPD}[3]{\mbox{{\bf T}}_{#1}\downarrow #2(#3)}
\newcommand{\TPJU}[4]{\mbox{{\bf T}}^{\mbox{#1}}_{#2}\uparrow #3(#4)}
\newcommand{\TPJD}[4]{\mbox{{\bf T}}^{\mbox{#1}}_{#2}\downarrow #3(#4)}
\newcommand{\TP}[1]{\mbox{{\bf T}}_{#1}}
\newcommand{\BL}[1]{\mbox{B}_{#1}}
\newcommand{\ggets}{\mbox{:=}}
\setcounter{page}{0}

\begin{document}
\thispagestyle{empty}
\begin{center}
{\Large {\bf Programming Language Comprehensive, August 21,
1997}}
\end{center}
\par
\noindent
{\large\sc Instructions}. Do all 6 questions. You have
4 hours.
\par
\skp{2}
\noindent
{\bf Question 1}:
Give a formal proof (or natural deduction
style proof-tree) that
the following specification is partially correct:
\[
\mbox{
\{true\}~N~:=~14518~;~{\bf while}~N~$>$~0~%
{\bf do}~N~:=~N~-~17~\{N~=~0~\}
}\,.
\]
Note that $14518 = 17 * 854$.
\par
\skp{2}
\noindent
{\bf Question 2}:  Suppose we have a programming language {\bf
P} and we provide a denotational semantics for it.  Suppose we
then go on to provide a formal system of axioms and rules.
Discuss the relationship between the denotational semantics and
the formal system of axioms and rules.  Give an example of the
denotation of the local definition block from Tennent's 
simple applicative language.  
What is the extensionality rule of inference?  Argue that it
is sound.  (For less credit, discuss the soundness of the rule
of inference for {\bf while} coommands in the simple imperative
language.)
\par
\skp{2}
\noindent
{\bf Question 3}:
\par
\skp{1}
\noindent
{\bf a)} 
Formulate an intuitively correct definition of 
\[
\lbrac\,\exists\,\mbox{Y}(\mbox{B})\,\rbrac \sigma
\]
where B is a boolean expression.
(`$\exists\,\mbox{Y}$' means `there exists Y'.)
\par
\skp{1}
\noindent
{\bf b)} Recall the form of the assignment axioms:
\[
\mbox{\{[B](X $\mapsto$ E)\} X := E \{B\}}\,.
\]
These axioms have a ``backward''
direction to them.  
In contrast, here is a form of ``forward'' axiom for
assignment 
statements:
\[
\mbox{\{B\} X := E \{$\exists\,$Y ([B](X $\mapsto$ Y) and X = [E](X
$\mapsto$ Y)\}}
\]
where Y is a variable that does not occur in B and does not
occur in E.
\par
\noindent
Assume that B is a boolean expression and
show that this axiom is valid.  
\par
\noindent
{\sc Hint}: The `Y' in the post condition is the ``old'' value
of X, i.e. the value of `X' before X~:=~E is executed. 
\par
\skp{2}
\noindent
{\bf Question 4}:  
Calculate and simplify as much as you can by following the
computational steps of a {\em plausible interpreter}\/ for the
simple imperative language:
\[
\mbox{
$\lbrac$ {\bf letrec} h : {\bf val}[{\bf nat}] $\rightarrow$ %
{\bf val}[{\bf nat}]
{\bf be} $\lambda\,$n:{\bf val}[{\bf nat}].%
{\bf if} n = 0 {\bf then} 1 {\bf else} g(h(n-1)) {\bf in}
h(2)%
$\rbrac\,$u
}
\]
Show all steps.  
\par
\skp{2}
\noindent
{\bf Question 5}:  Give an example of a syntactical
programming language construct which is NOT context-free, and
briefly sketch an explanation for your example.
\par
\skp{2}
\noindent
{\bf Question 6}:  
\par
\skp{1}
\noindent
{\bf a)} Define {\em domain}.  If you have in my mind a
particular book or paper for this definition, tell which one.
\par
\skp{1}
\noindent
{\bf b)} A {\em directed set} is a nonempty 
subset $A$ of a partially ordered
set $D$ with the property that every two elements in $A$ have
an upper bound in $A$.  A partially ordered set $D$ is
{\em complete} if every directed subset of $D$ has a least upper
bound in $D$.  Denote the least upper bound of a set $A$ by
$\bigsqcup A$.  We call a partially ordered set which is
complete a dcpo.  (This stands for {\em directed-complete
partial order}.)  Let $D$ and $E$ be dcpo's.  A function 
$f : D \longrightarrow E$ is a {\em compact} iff $\{f(a) \mid a
\in A\}$ is directed and $f(\bigsqcup A) \sqsubseteq \bigsqcup%
\{f(a) \mid a \in A\}$ for all directed subsets of $D$.
Give an example of a function which is compact, but not
monotone.  You must specify $f$, $D$ and $E$.
\end{document}
