\documentclass[12pt]{cas-handout}
\usepackage{amsfonts}
\usepackage{paralist}

\newtheorem{theorem}{Theorem}

\anumber{6}
\title{Temporal Logic and Cardinality}
\duedate{11:00am, Wednesday, October 31}



\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{Temporal Logic}

(CTL was described in class.  It also appears in Section~3.4 of Huth \& Ryan.)

\begin{center}
  \includeimage{CTL-Summary}
\end{center}

\clearpage
\noindent Consider the possible execution paths in the following piece of C/C++/Java-style code:
{
\begin{Verbatim}[frame=single]
 int a[100] = { 0, 0, 0, ..., 0 };  // Array is initially all zeros

 while (true) {
     int k = user_input();   // Assume this user input will be a number
                             //      between 0 and 99 inclusive!

     if (a[k] == 1) {
          // Reset the array back to zeros
          for (int i = 0; i < 100; ++i)
               a[i] = 0;
     } else {
          // Set the k-th element of the array to 1
          a[k] = 1;
     }
 }
\end{Verbatim}
}

\noindent
Which of the following logical propositions are true (starting at the
beginning of the program)?  Explain your answer; you
do not need to provide a full formal proof, but your explanation
should be clear and convincing.

\begin{enumerate}
\item $AG\ (\mathtt{a[42]} = \mathtt{0})$

\item $AG\ \left({\displaystyle \sum_{j=0}^{j < 100} \mathtt{a[}j\mathtt{]}
    \ \ \ < \ \ \ 100}\right)$

\item $EF\ (\mathtt{a[42]} = \mathtt{1})$

\item $AF\ (\mathtt{a[42]} = \mathtt{1})$

\item $EG\ (\mathtt{a[42]} = \mathtt{0})$

\item $AG\ (AF\ (\mathtt{a[42]} = \mathtt{0}))$

\item $AG\ (EF\ (\mathtt{a[42]} = \mathtt{1}))$

\item $EF\ (AG\ (\mathtt{a[42]} = \mathtt{0}))$

\end{enumerate}

\section{Cardinality}

Carefully argue whether the following sets are
countable or not.
\begin{enumerate}
\item The set of partial functions from $\mathbb{N}$ to $\mathbb{N}$
whose support is a finite set.

  [A total function is one that, for any input, produces an output.
  A \emph{partial} function
  is one that, for some or all particular inputs, always returns
  ``don't know'' or ``undefined'' (often written
  $\bot$ although it's not a truth value)
  rather than returning an output.
   The \emph{support} of a partial function (sometimes called
  the domain or domain of definition) is the collection
  of inputs that provide non-$\bot$ output.

  For example, we could have a partial function $\mathsf{sqrt}: \mathbb{R}
  \rightharpoonup \mathbb{R}$ defined by
\[
\mathsf{sqrt}(x) :=
\begin{cases}
  \sqrt{x} & \mbox{if }x\ge 0;\\
  \bot & \mbox{otherwise.}\\
\end{cases}
\]
The support of $\mathsf{sqrt}$ is then the set of all nonnegative
real numbers.]

\item The set all valid Hoare Logic proofs.

\item The set of flow networks with rational capacities (directed graphs
  with finitely many nodes and edges,
  where each directed edge is labeled with a rational number
  called the ``capacity'' of that edge).

\item The set of Java programs that typecheck (i.e., that succesfully compile to a Java .class file)

\end{enumerate}

\end{document}
