\documentclass[boldsans]{article}
\usepackage{ccfonts,amsmath,amssymb,fullpage}
\usepackage{hyperref}
\hypersetup{pdfpagemode=Fullscreen,
  colorlinks=true,
  linkfileprefix={}}
\title{CSC236, Fall 2012\\
Assignment 3}
\renewcommand{\today}{~}
\begin{document}
\maketitle

These problems are to give you some practice with correctness proofs,
and regular languages.  Start early, and seek out your instructor and
teaching assistant when you have questions.

Submit your solutions as a PDF file called \texttt{a3.pdf}.
You must generate the PDF from a word processor, or LaTeX --- no
scanned handwritten work will be accepted.
\begin{enumerate}
\item Let $L=\{x\in\{0,1\}^* \mid \text{fourth-last symbol in }x\text{
    is }0\}$.  Prove that any DFSA that accepts $L$ has at least 16
  states.  \textbf{Hint:} Consider the sixteen binary strings of
  length four, and what happens if two of them drive a DFSA to the
  same state.

\item Prove that the following terminates, given the precondition
  $x\in\mathbb{N}$:
\begin{verbatim}
y = x * x
while not y == 0 :
  x = x - 1
  y = y - 2 * x - 1
\end{verbatim}
\textbf{Hint:} Trace through the code for a few small values of $x$,
then derive (and prove) a loop invariant that helps prove
termination.

\item Design a DFSA that accepts the language of binary strings over
  $\{0,1\}$ that have a multiple of 4 1s.  Devise, and prove a state
  invariant, and explain how it shows that your DFSA accepts this
  language.

\item Design an iterative binary search algorithm that is correct with
  respect to the following precondition/postcondition pair:
  \begin{description}
  \item[Precondition:] $A$ has elements that are comparable with $x$,
    $|A|=n>0$, and $A$ is sorted in non-decreasing order.
  \item[Postcondition:] binSearch($x$, $A$) terminates and returns an
    index $p$ that satisfies:
    \begin{eqnarray*}
      A[0 \ldots p] &\leq& x < A[p+1 \ldots n-1] \\
      -1 &\leq& p \leq n-1
    \end{eqnarray*}
    Prove that if the precondition is satisfied, then your algorithm
    terminates and satisfies the postcondition.
    \textbf{Hint:} Use the approach from lecture (no need to provide
    the pictures) where you develop a loop invariant as you write the
    code.
  \end{description}
\end{enumerate}
\end{document}
