\documentclass[11pt]{article}
\input{/home/cisfac/blair/TeX/macros}
\newcommand{\triple}[3]{\ensuremath{\{#1\}\mathit{#2}\{#3\}}}
\newcommand{\implies}{\ensuremath{\Longrightarrow}}
\newcommand{\tightenlist}{\itemsep=2pt\topsep=0pt\parskip=0pt}
\newcommand{\ggets}{\mbox{:=}}
\newcommand{\lbrac}{[\![}
\newcommand{\rbrac}{]\!]}


\begin{document}
\begin{center}
  {\Large Semantics of Programming Languages Comprehensive Exam}
 
  {January, 1999}
\end{center}

\section*{Instructions}
Answer all parts of all questions; you have four hours.
 
To maximize partial credit for an incomplete proof, you
should:
\vspace*{-1.25ex} 
\begin{itemize} \tightenlist
\item provide as much of the proof as you can; 
\item describe what remains to be proven and how that (when
combined
  with what you have proven) would complete the proof;
\item indicate (where possible) how you suspect that the
missing piece
  \emph{could} be proven.
\end{itemize}
 
The last two pages of this exam include a summary of relevant
terminology  and partial-correctness inference rules.
 
 
 
\section*{Questions}
\newcommand{\blet}{\ensuremath{\mathbf{let\ }}}
\newcommand{\bbe}{\ensuremath{\mathbf{be\ }}}
\newcommand{\bin}{\ensuremath{\mathbf{in\ }}}
\newcommand{\sem}[1]{\ensuremath{[\![#1]\!]}}

\noindent
{\bf 1a)}  Is the following equivalence valid?
\[
\mbox{
({\bf for} N {\bf do} N := N+1) $\equiv$ {\bf diverge}
}
\]
If the equivalence is valid, prove it.  If it is invalid, give
a couner-example and explain why your counter-example shows 
the equivalence is invalid.
\par
\skp{2}
\noindent %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
{\bf 1b)} Is the following equivalence valid?
\[
\mbox{
({\bf if} B {\bf then} C$_{1}$ {\bf else} C$_{2}$); C$_{3}$ 
$\equiv$ {\bf if} B {\bf then} (C$_{1}$;C$_{3})$ {\bf else} 
(C$_{2}$;C$_{3}$)
}
\]
If the equivalence is valid, prove it.  If it is invalid, give
a couner-example and explain why your counter-example shows 
the equivalence is invalid.
\par
\skp{2}
\noindent %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
{\bf 2)}  Let $D$ be a domain with partial order relation
$\sqsubseteq$.
\par
\noindent
{\bf Definition:} Let $f : D \longrightarrow D$ and let $d \in D$. 
$f$ is {\em increasing at} $d$ if $d \sqsubseteq f(d)$.  
An element $e$ of $D$ is the {\em least fixed point}
of $f$ {\em above} $d$ if
\begin{itemize}
\item $d \sqsubseteq e$,
\item $f(e) = e$,
\item for all $e'$ such that $d \sqsubseteq e'$: 
$f(e') = e'$ implies $e \sqsubseteq e'$.
\end{itemize}
Denote the least fixed point of $f$ above $d$, if it exists,
by $\mbox{\em fix}_{d}(f)$.
\par
\skp{1}
\noindent
{\bf Proposition:} If $f : D \longrightarrow D $ is continuous, and
increasing at $d$, then $\mbox{\em fix}_{d}(f)$ exists and
\[
\mbox{\em fix}_{d}(f) = \bigsqcup^{\infty}_{i=0}f^{i}(d)\,.
\]
\par
\noindent
{\bf Part a)} Prove the proposition.
\par
\skp{2}
\noindent
{\bf Part b)} Let $f,g : D \longrightarrow D$ be continuous
functions on $D$ that are both increasing at $d$.  Prove that
all of the fixed points in the following equation exist, and
that the equation holds:
\[
g(\mbox{\em fix}_{d}(f \circ g)) = \mbox{\em fix}_{d}(g \circ f)\,.
\]
\par
\skp{2}
\noindent
{\bf 3)} Give a formal proof in Floyd-Hoare logic (see
attachment) that the following command is partially correct with
respect to the indicated pre- and post-conditions.
\begin{quote}
$\{\mbox{A} \geq 0\}$\\
X $\ggets$ 0;\\
Y $\ggets$ A;\\
{\bf while} $\mbox{X} < \mbox{Y}$ {\bf do}\\
\hspace*{0.8cm} (Y $\ggets$ Y - 1; X $\ggets$ X + 1);\\
$\{\mbox{Y} = \mbox{A div 2}\}$
\end{quote}
\par
\skp{2}
\noindent
{\bf 4)}  
Let $D_{\bot} = \{a,b,\bot\}$ be a domain with bottom element
$\bot$.  Thus, $\bot \sqsubseteq a$ and $\bot \sqsubseteq b$. Suppose 
that $a$ and $b$ are incomparable in the partial order $\sqsubseteq$.  
Let $S = \{x,y\}$. $S$ is just a set without any ordering.
\par
\skp{1}
\noindent
{\bf Part a)} List the elements in the set of functions 
$S \longrightarrow D_{\bot}$
and describe the ordering among them in the ``pointwise''
ordering that is determined by $\sqsubseteq$.  Note that each
element that you must list is a function, and that a function
can be described by listing the ordered pairs in its graph.
\par
\skp{1}
\noindent
{\bf Part b)} Now let $D$ and $E$ be domains with bottom elements.
A function $f : D \longrightarrow E$ is {\em strict} if $f(\bot_{D})
= \bot_{E}$. Suppose $D$ has exactly $1000$ elements and $E$
has exactly $50$ elements.  How many functions in the set of functions
$D \longrightarrow E$ (the set of all functions from $D$ to
$E$) are strict?
\newpage
\noindent
\section*{Terminology}

A \emph{domain} (technically, an $\omega$-complete partial order) is a pair
$(D,\sqsubseteq)$ such that:
  \begin{itemize}
  \item $\sqsubseteq$ is a partial order
  \item $D$ has a least element $\bot_D$
  \item Every chain $x_0 \sqsubseteq x_1 \sqsubseteq \cdots \sqsubseteq
    x_n \sqsubseteq \cdots$ in $D$ has a supremum (least upper bound).
  \end{itemize}

A function $f :D \rightarrow E$ between domains $(D,\sqsubseteq_D)$ and
  $(E,\sqsubseteq_E)$ is \emph{continuous} if, for all chains in $D$,
  \[ f(\bigsqcup_{n=0}^\infty x_n) = \bigsqcup_{n=0}^\infty f(x_n). \]

A \emph{fixed point} of a function $f: D\rightarrow D$ is an
  element $x\in D$ such that $f(x)=x$.  A \emph{least fixed point} of
  $f$ is a fixed point $x$ such that, for all other fixed points $y$,
  $x\sqsubseteq y$.
  
  The least fixed point of a continuous function $f$, denoted
  $\mathit{fix(f)}$, can be calculated by
  \[ \mathit{fix}(f) = \bigsqcup_{n=0}^\infty f^n(\bot). \]


\section*{Axioms and Rules of Inference for Floyd-Hoare Logic}

These axioms are taken directly from Tennent's \emph{Semantics of
  Programming Languages}.

\subsection*{Command-specific axioms and rules of inference}

\noindent

\triple{P}{skip}{P} \vspace*{1ex}

\triple{\mathsf{true}}{diverge}{\mathsf{false}} \vspace*{1ex}

\triple{[P](\iota \mapsto E)}{\iota := E}{P} \vspace*{1ex}

\triple{P}{C}{Q} \implies \triple{P}{(C)}{Q} \vspace*{1ex}

\triple{P}{C_0}{Q} \& \triple {Q}{C_1}{R} \implies
\triple{P}{C_0;C_1}{R} \vspace*{1ex}

\triple{P \mathsf{\ and\ } B}{C_0}{Q} \& 
\triple{P \mathsf{\ and\ not\ } B}{C_1}{Q} \implies 
\triple{P}{if\ B\ then\ C_0\ else C_1}{Q}  \vspace*{1ex}


\triple{P \mathsf{\ and\ } B}{C}{P} \implies
\triple{P}{while\ B\ do\ C}{P\mathsf{\ and\ not\ } B}  \vspace*{1ex}


\subsection*{Other axioms and rules of inference}
\noindent

Pre-condition Strengthening: \vspace*{1ex}

$P_0 \supset P_1$ \&  \triple{P_1}{C}{Q}  \implies \triple{P_0}{C}{Q}
\vspace*{1ex}


Post-condition Weakening:
\vspace*{1ex}

$Q_0 \supset Q_1$ \&  \triple{P}{C}{Q_0}  \implies \triple{P}{C}{Q_1}
\vspace*{1ex}

Pre-condition Disjunction:
\vspace*{1ex}

\triple{P_1}{C}{Q} \& $\cdots$ \& \triple{P_n}{C}{Q} \implies
 \triple{P_1 \mathsf{\ or\ } \cdots \mathsf{or\ } P_n}{C}{Q} 
\vspace*{1ex}

Post-condition Conjunction:
\vspace*{1ex}

\triple{P}{C}{Q_1} \& $\cdots$ \& \triple{P}{C}{Q_n} \implies
 \triple{P}{C}{Q_1 \mathsf{\ and\ } \cdots \mathsf{and\ } Q_n} 
\vspace*{1ex}

\subsection*{Semantics of some commands}
$\ $

$\lbrac(X)\rbrac = \lbrac X \rbrac$\,.
\vspace*{1ex}

$\lbrac\, \mbox{\bf if}\ B\ \mbox{\bf then}\ X_{0}\ \mbox{\bf
else}\ X_{1}\,\rbrac s = 
\left\{ \begin{array}{cc}
       \lbrac X_{0} \rbrac s & \mbox{if}\ \lbrac B \rbrac =
\mbox{\em true}\\
       \lbrac X_{1} \rbrac s & \mbox{if}\ \lbrac B \rbrac =
\mbox{\em false}
       \end{array}
\right.$
\vspace*{1ex}

$\lbrac\mbox{\bf true}\rbrac s = \mbox{\em true}$
\vspace*{1ex}

$\lbrac\mbox{\bf not}\ B\rbrac s =
\left\{ \begin{array}{cc} 
       \mbox{\em false} & \mbox{if}\ \lbrac B \rbrac s = 
\mbox{\em true}\\
       \mbox{\em true}  & \mbox{if}\ \lbrac B \rbrac s =
\mbox{\em false}
       \end{array}
\right.$
\vspace*{1ex}

$\lbrac B_{0}\ \mbox{\bf and}\ B_{1}\rbrac s = 
(\lbrac B_{0}\rbrac s\ \mbox{and}\ \lbrac B_{1}\rbrac s)$
\vspace*{1ex}

$\lbrac N_{0} < N_{1} \rbrac s = (\lbrac N_{0}\rbrac s < 
\lbrac N_{1} \rbrac s)$
\vspace*{1ex}

$\lbrac E_{0} = E_{1} \rbrac s = (\lbrac E_{0} \rbrac s < 
\lbrac E_{1} \rbrac s)$
\vspace*{1ex}

$\lbrac 0 \rbrac s = 0$
\vspace*{1ex}

$\lbrac \mbox{\bf succ}\ N \rbrac s = (\lbrac N \rbrac s) + 1$
\vspace*{1ex}

$\lbrac \mbox{\bf skip} \rbrac s = s$ 
\vspace*{1ex}

$\lbrac C_{0};C_{1} \rbrac s = \lbrac C_{1} \rbrac (\lbrac
C_{0} \rbrac s)$
\vspace*{1ex}

$\lbrac\, \mbox{\bf for}\ N\ \mbox{\bf do}\ C\, \rbrac s =
\lbrac C \rbrac^{\lbrac N \rbrac s}(s)$
\vspace*{1ex}

$\lbrac \mbox{\bf diverse} \rbrac s$ is undefined, for all
states $s$.

\end{document}










