\documentclass[12pt]{article}
\usepackage{advpl}

\setlength\voffset{-2cm}
\addtolength\textheight{3cm}
\def\rarr{\longrightarrow}
\title{Advanced Programming Languages \\ Homework Assignment 4} 
\date{}

\begin{document}

\maketitle

\def\VC{\mathrm{VC}}
\def\WP{\mathrm{WP}}

\exercise In class we gave the following rules for the (backward)
verification condition generation of assignment and let:
\[
\begin{array}{ll}
\VC( c_1 ; c_2, B)                  & = \VC(c_1, \VC(c_2, B)) \\
\VC( x := e, B)                  & = [e/x]~B \\
\VC( \mathsf{let~} x = e \mathsf{~in~} c, B)          & = [e/x]~\VC(c,B) 
\end{array}
\]
That rule for $\mathsf{let}$ has a bug. Give a correct rule for
$\mathsf{let}$. 

\exercise {\bf Extra Credit.} 
Given $\{A\} c \{B\}$ we desire that $A \implies \VC(c,B) \implies
\WP(c,B)$.  We say that our $\VC$ rules are \emph{sound} if 
$\models \{ \VC(c,B) \}~c~\{ B \}$. Demonstrate the unsoundness of the
buggy $\mathsf{let}$ rule by giving the following six things: 
\begin{enumerate}
\item a command $c$ and 
\item a post-condition $B$ and 
\item a state $\sigma$ such that 
\item $\sigma \models \VC(c,B)$ and 
\item $\langle c, \sigma \rangle \Downarrow \sigma'$ but 
\item $\sigma' \not \models B$. 
\end{enumerate} 

\exercise Write a sound and complete Hoare rule for $\mathsf{do~} c
\mathsf{~while~} b$. This statement has the standard semantics (e.g., $c$
is executed at least once, before $b$ is tested). 

\exercise Choose exactly \emph{one} of the 4A and 4B below. (If you are not
certain, pick 4A. The answers end up being equivalent, but 4A may be easier
to grasp for some students and 4B easier to grasp for others.) 

\begin{itemize}

\item[4A.]
Give the (backward) verification condition formula for the command
$\mathsf{do}_{\mathit{Inv}}~c~\mathsf{while~}b$ with respect to a
post-condition $P$. The invariant $\mathit{Inv}$ is true before each
evaluation of the predicate $b$. Your answer may not be defined in terms of
$\VC(\mathsf{while} ...)$. 

\item[4B.]
Give the (backward) verification condition formula for
the command
$\mathsf{do}_{\mathit{Inv1},\mathit{Inv2}}~c~\mathsf{while~}b$
with respect to a post-condition $P$. The invariant $\mathit{Inv1}$ is true
before $c$ is first executed. The invariant $\mathit{Inv2}$ is true before
each evaluation of the loop predicate $b$.  Your answer may not be defined
in terms of $\VC(\mathsf{while} ...)$. 

\end{itemize} 


\exercise Consider the following three alternate $\mathsf{while}$ Hoare
rules (named $\mathsf{lannister}$, $\mathsf{stark}$, and
$\mathsf{targaryen}$):
\[
\infer[\mathsf{lannister}] 
  {\vdash \{ b \implies X \aand \neg b \implies Y \} \mathsf{while}\;b\;\mathsf{do}\;c \; \{ Y \}}
  {\vdash \{ X \}\;c\; \{ b \implies X \aand \neg b \implies Y\}}
\qquad
\infer[\mathsf{stark}]
        {\vdash \{ X \} \mathsf{while}\;b\;\mathsf{do}\;c \; \{ X \}}
      {\vdash \{ X \aand b \}\;c\; \{ X \}}
\]
\[
\infer[\mathsf{targaryen}]
        {\vdash \{ X \} \mathsf{while}\;b\;\mathsf{do}\;c \; \{ X \aand \neg b\}}
      {\vdash \{ X \}\;c\; \{ X \}}
\]
All three rules are sound but incomplete. Choose two
incomplete rules. For each chosen rule provide the following: 
\begin{enumerate}
\item the name of the rule and 
\item $A$ and
\item $B$ and
\item $\sigma$ and
\item $\sigma'$ and
\item $c$ such that
\item $\langle c, \sigma \rangle \Downarrow \sigma'$ and
\item $\sigma \models A$ and 
\item $\sigma' \models B$ but 
\item it is not possible to prove $\vdash \{ A \}~c~\{ B \}$. 
\end{enumerate} 

\emph{Flavor text:} Incompleteness in an axiomatic semantics or type system is
typically not as dire as unsoundness. An incomplete system cannot prove all
possible properties or handle all possible programs. Many research results
that claim to work for the C language, for example, are actually incomplete
because they do not address \t{setjmp}/\t{longjmp} or bitfields. (Many of
them are also unsound because they do not correctly model unsafe casts,
pointer arithmetic, or integer overflow.)  

\exercise No coding component. Instead, tell me how long you spent on this,
something you like about the class (or the work, or the project, or
whatever), something you do not like, and something I do not know about
you. All non-null answers receive full credit. Think about your project
proposal. 

\end{document}