\documentclass[10pt]{article}

%\usepackage{fullpage}
\topmargin 0pt
\advance \topmargin by -\headheight
\advance \topmargin by -\headsep
     
\textheight 8.9in
     
\oddsidemargin 0pt
\evensidemargin \oddsidemargin
\marginparwidth 0.5in
     
\textwidth 6.5in

\newcommand{\triple}[3]{\ensuremath{\{#1\}\mathit{#2}\{#3\}}}
\newcommand{\implies}{\ensuremath{\Longrightarrow}}
\newcommand{\tightenlist}{\itemsep=2pt\topsep=0pt\parskip=0pt}

\begin{document}
\begin{center}
  {\Large Programming Languages Comprehensive Exam}

  {August, 1998}
\end{center}

\section*{Instructions}
Answer 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]\!]}}

\begin{enumerate}
\item Prove the following law of program equivalence by using the
  valuation for local-definition blocks:
  \[ \blet \iota\ \bbe P\ \bin ( \blet \iota\ \bbe Q\ \bin R)\ \equiv\
     \blet \iota\ \bbe (\blet \iota\ \bbe  P\ \bin Q)\ \bin R \]

  That is, show that 
  \[ \sem{\blet \iota\ \bbe P\ \bin\ ( \blet \iota\ \bbe Q\ \bin R)}u
    = \sem{\blet \iota\ \bbe (\blet \iota\ \bbe  P\ \bin Q)\ \bin R}u \]
  for all $u$.  Be sure to show all steps of your computation.

\item Prove (using the valuation for local-definition blocks) or
  disprove (by providing \emph{and explaining} a counterexample) the
  following potential law of program equivalence:
  \[ \blet \iota\ \bbe P\ \bin ( \blet \iota'\ \bbe Q\ \bin R)\ \equiv\
     \blet \iota'\ \bbe (\blet \iota\ \bbe  P\ \bin Q)\ \bin ( \blet
     \iota\ \bbe P\ \bin R) \] 


\item Let $f,g: D\rightarrow D$ be continuous functions over a domain
  $(D,\sqsubseteq)$.
  
  \begin{enumerate}
  \item Prove that $f (\mathit{fix} (g \circ f)) = \mathit{fix} (f\circ g)$.
  \item An element $x\in D$ is a \emph{least common fixed point} of $f$
    and $g$ if it is a fixed point of both $f$ and $g$ and it is least
    among all such points.  That is, the \emph{least common fixed point}
    of $f$ and $g$ (when it exists) is an element $x\in D$ such that:
    \begin{itemize}
    \item $f x = x$ and $g x = x$;
    \item for all $y$ such that $f y = y$ and $g y = y$,  $x\sqsubseteq y$.
    \end{itemize}
  
    Prove that, if $f\circ g = g \circ f$, then $f$ and $g$ have a least
    common fixed point.
  \item Let $(D,\sqsubseteq)$ be the domain given by $D = \{\bot,
      \mathrm{tt}, \mathrm{ff}, \top\}$ ordered as follows: \vspace*{2ex}

      \hspace*{2in}
      \unitlength = 5pt
      \begin{picture}(10,10)(-5,-5)
        \put(-5,0){\makebox(0,0){tt}}
        \put(5,0){\makebox(0,0){ff}}
        \put(0,-5){\makebox(0,0){$\bot$}}
        \put(0,5){\makebox(0,0){$\top$}}

        \put(-4,1){\line(1,1){3}}
        \put(-4,-1){\line(1,-1){3}}
        \put(4,1){\line(-1,1){3}}
        \put(4,-1){\line(-1,-1){3}}
      \end{picture}

      Give a pair of continuous functions $f,g: D \rightarrow D$ such
      that $f \circ g = g \circ f$ and the least common fixed point of
      $f$ and $g$ is different from the least fixed point of $f$ and the
      least fixed point of $g$.
    \item Using $(D,\sqsubseteq)$ from part (c), show that the converse
      to part (b) is not true.  That is, give a pair of continuous
      functions $f,g: D \rightarrow D$ such that $f$ and $g$ have a
      least common fixed point but $f \circ g \neq g \circ f$.
  \end{enumerate}



  
\item  The construct \textit{repeat C until B} provides a looping
  mechanism in which the loop's body is always executed at least once.  
  In particular, the construct satisfies the following program
  equivalence: 
  \[ \mathit{repeat\ C\ until\ B} \;\equiv\;
         \mathit{C;\ if\ B\ then\ skip\  else\ (repeat\ C\ until\ B)} \]

  \begin{enumerate}
  \item Explain how you would define the semantic valuation
    \sem{\mathit{repeat\ C\ until\ B}} \emph{compositionally}.  You can
    state your semantics in English rather than using mathematical
    notation if you prefer, but your answer should provide enough detail
    to make explicit your intended semantics and its compositional
    nature.
    
  \item Give a valid axiom (in the style of Tennent) suitable for
    reasoning about the partial correctness of programs including this
    construct.

  \item Use your axiom (along with the axioms on the attached sheet) to
    provide a rigorous proof of the validity of the following
    partial-correctness Hoare formula:

  \hspace*{1in}
  \textit{
    \begin{minipage}[t]{15em}
      \begin{tabbing}
        $\{ y\geq 0\}$ \\
        z := 0;\ w := x;\ k := y; \\
        repeat \=  \\
              \> if \= even(k) \\
              \>    \> then (k := k div 2; w := w + w) \\
              \>    \> else (k := k - 1; z := z + w)   \\
        until  $k = 0$ \\
        $\{z = x\ast y\}$
      \end{tabbing}
    \end{minipage}
    }

  You may use without proof any facts about the integers, as well as the
  following derived law:

  \[ \triple{[\cdots[ [P](\iota_n \mapsto E_n)]\cdots](\iota_1\mapsto
    E_1)}{\iota_1:= E_1;\cdots;\iota_n := E_n)}{P} \]
  \end{enumerate}

  
\end{enumerate}

\newpage
\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 for Floyd-Hoare Logic}

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

\subsection*{Command-specific axioms}

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

\end{document}
