\documentstyle[10pt,epsf,fuzz]{article}

\input{./handout}

\newtheorem{defn}{Definition}
\newenvironment{spec}{
 \vspace*{8pt}
 \begin{center}
 \begin{minipage}{5in}
 \renewcommand{\baselinestretch}{1}
 }{
 \end{minipage}
 \end{center}
 \vspace*{8pt}
}

\begin{document}

\homework{8}{25 October 1995}{Abstraction; Algebraic Reasoning}

\begin{symbolfootnotes}
\footnotetext[0]{\copyright 1995 Jeannette M. Wing and David Garlan} 
\end{symbolfootnotes}

This homework looks long but Problem 1 is really, really easy
and Problems 3 and 4 are (meant to be) easy.  Problem 2 is relatively
straightforward.

\problem{1}

Prove that Counter satisfies Light (see handout on State Machine
Basics).

\problem{2}

The following questions refer to the Register problem that you did
in HW 6. Consider a concrete implementation of the register state
space that represents the class register as two sequences: one that
contains the enrolled students, and the other that is a sequence of
YES or NO, indicating whether the corresponding student has completed
the course.

a. Write a schema to model the concrete state space. Think carefully
about the representation invariant.

b. Also write a schema representing the initial state. Argue
(informally) that the Initialization Theorem holds for this schema
(i.e., there exists a state space satisfying the intial conditions.)

c. Write down (as a schema) the abstraction relation that relates the
concrete state space and the previous abstract state space.

d. Explain why your concrete representation is ``adequate.''

e. Argue that the initial state is a reasonable concrete
representation by showing that it corresponds to the initial state of
the abstract state space.

f. Produce a concrete version of AddStudent.

g. Argue informally (in the style of Spivey's paper, and the
lecture slides) that this concrete operation is correct. (Hint: first
show that the operation is ``adequate''-- defined over an
appropriate set of concrete states; then show that it produces results
that are consistent with the abstract operation.)

\problem{3}
Refer to p. 19 of the Larch handout.

a. What Bool terms do the following terms reduce to?

\begin{verse}
i2 $\in$ add(add(new, i1, v1), i2, v2) = ? \\
i2 $\in$ add(add(new, i2, v2), i1, v1) = ? \\
i3 $\in$ add(add(new, i1, v1), i2, v2) = ? \\
i1 $\in$ add(add(add(new, i1, v1), i2, v2), i1, v3) = ?
\end{verse}

b. What Val terms do the following terms reduce to?

\begin{verse}
lookup(add(add(new, i1, v1), i2, v2), i2) = ? \\
lookup(add(add(new, i2, v2), i1, v1), i2) = ? \\
lookup(add(add(new, i1, v1), i2, v2), i1) = ? \\
lookup(add(add(add(new, i1, v1), i2, v2), i1, v3), i1) = ?
\end{verse}

\newpage

c. What Int terms (values) do the following terms reduce to?

\begin{verse}
size(add(add(new, i1, v1), i2, v2)) = ? \\
size(add(add(new, i2, v2), i1, v1)) = ? \\
size(add(add(add(new, i1, v1), i2, v2), i1, v3)) = ?
\end{verse}

d. Is ``add'' commutative?  (Does it matter in which order I add (i, v) bindings to my table?)
Why or why not?

e. Can I tell if multiple copies of the same (i, v) binding are stored in my table?
Why or why not?

f. Can multiple values be associated with a single index?
Why or why not?


\problem{4} 

Exercise 11.7, part 1 of Woodcock and Loomes (page 223).  Just define enough
operations on sequences needed to show that the left-hand side
rewrites to the right-hand side.

\end{document}