CMU 15-671Models of Software SystemsFall 1995
Abstraction; Algebraic Reasoning
Garlan & Wing Homework 8 Due: 25 October 1995
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?
i2 
add(add(new, i1, v1), i2, v2) = ?
i2 add(add(new, i2, v2), i1, v1) = ?
i3 add(add(new, i1, v1), i2, v2) = ?
i1 add(add(add(new, i1, v1), i2, v2), i1, v3) = ?
b. What Val terms do the following terms reduce to?
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) = ?
c. What Int terms (values) do the following terms reduce to?
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)) = ?
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.