\documentclass[11pt]{cas-handout}
\usepackage{alltt}
\usepackage{paralist}
\usepackage{mathpartir}

\newtheorem{theorem}{Theorem}
\newcommand{\BAR}{\ |\ }

\anumber{7}
\title{Strings, Languages, and Induction}
\duedate{11:00am, Wednesday, November 7}



\begin{document}
\maketitle

\begin{itemize}
  \item Emails about this assignment should be directed to
    \helpalias.
 \item The usual collaboration rules apply. You may \emph{discuss} an
    exercise with any other student(s) currently taking CS 81 as long as:
    \begin{compactitem}
      \item You contribute equally;
      \item You come away from this discussion only with
        \emph{understanding in your head} --- no written materials or
        computer notes may be retained;
      \item Your submission is authored solely by you, on a separate
        occasion.
   \end{compactitem}
  \item You should refer only to materials from this semester of CS 81 (lecture
   notes, handouts, textbooks, grutors, profs, etc.).
 \item Bring a writeup/printout to class on the due date. Illegible answers
    will get no credit.
\item Make sure your submission includes your name!
\end{itemize}

\section{Structural Induction on Programs}

The midterm reviewed the imperative language of ``commands''
in our Hoare Logic proofs, and asked how induction could be
used to prove that every command satisfies some property

Show that $\top$ works as a postcondition for every command, by using
structural induction to prove that every command $c$ satisfies:

\begin{center}
  ``for every logical precondition $A$, there is\\ a Hoare Logic proof
  whose conclusion is $\{\ A\ \}\ c\ \{\ \top\ \}$''
\end{center}
}

Your proof should be in ``mathematical English'' (rather than
a natural deduction or tableau proof).
For reference, the relevant rules of Hoare Logic are repeated here:
{%\small
\begin{mathpar}

\inferrule*[right=assign]{  }
           { \{\ P[e/x]\ \}\ \ \mbox{\tt $x$ = $e$}\ \ \{\ P\ \}}


\inferrule*[right=implied]{ P \to P' \\ \{\ P'\ \}\ c\ \{\ Q'\ \} \\ Q' \to Q }
           { \{\ P\ \}\ \ c\ \ \{\ Q\ \}}


\inferrule*[right=composition]{ \{\ P\ \}\ c_1\ \{\ R\ \} \\ \{\ R\ \}\ c_2\ \{\ Q\ \} }
           { \{\ P\ \}\ \ c_1; c_2\ \ \{\ Q\ \}}


\inferrule*[right=if]{ \{\ P \land e\ \}\ c_1\ \{\ Q\ \} \\ \{\ P \land \lnot e\ \}\ c_2\ \{\ Q\ \} }
           { \{\ P\ \}\ \ \mbox{\tt if ($e$):\,$c_1$ else:\,$c_2$}\ \ \{\ Q\ \}}


\inferrule*[right=while]{ \{\ I \land e\ \}\ \ c\ \ \{\ I\ \} }
           { \{\ I\ \}\ \ \mbox{\tt while ($e$):\,$c$}\ \ \{\ I \land \lnot e\ \}}

\end{mathpar}
}
\clearpage

\section{Deterministic State Machines}

Use the idea of derivatives/intrinsic states to draw ``minimal'' deterministic state machines for the following languages:
\begin{itemize}
  \item $L = \{\ w\in\{a,b\}^*\ |\ w \mbox{\ has an even number of a's and an odd number of b's}\ \}$
  \item $L = \{\ a^nb^n\ |\ n \ge 0\ \}$
\end{itemize}

\section{Nondeterministic State Machines}

\item Draw NFAs (NDFSMs) for the following languages, with the specified
  number of states. You may assume the alphabet is always $\{0,1\}$.

\begin{enumerate}
\item The language $\{\ w \BAR \mbox{$w$ ends in $00$}\ \}$, 3 states
\item The language $\{\ w \BAR \mbox{$w$ contains the substring
    $0101$}\ \}$, five states
\item The language $\{\ w \BAR \mbox{$w$ contains an even number of
    $0$s or exactly two  $1$s}\ \}$, six states
\item The language $\{0\}$, two states
\item The language $0^*1^*0^+$, three states
\item The language $1^*(001^+)^*$, three states
\item The language $\{\epsilon\}$, one state
\item The language $0^*$, one state
\end{enumerate}


\end{document}
