Due Wednesday February 17, 1999
What is wp(if C then S endif,Q)?
Briefly discuss how recursion would be handled in a program correctness proof? (Hint: One way to approach this is to look at analogs to how loops are handled.)
Consider the computation that takes a non-negative integer N and computes the sum of all the integers from 1 to N. As you may remember, the closed form solution for this is N*(N+1)/2.
Using induction, prove this closed form is correct.
Write a simple program, using the basic programming language structures including (at most) assignment, while loop, and if-then-else (with no side effects, etc.), that computes this sum.
Using Dijkstra weakest preconditions or Hoare triples, prove that your program is (weakly) correct. (That is, you don't have to prove termination. If you want, you can do this for a small amount of extra credit.)
Briefly discuss the relation, if any, between the proof of the program and the inductive proof of the correctness of the closed form.
Functional and logic programming languages are often said to be "declarative" rather than "imperative"; very roughly, it is said that they describe "what" is wanted rather than "how" it is achieved. This, of course, is also how formal specifications are characterized in contrast to programming languages.
For one of the following languages---ML, Haskell, pure Lisp, Prolog, or some other language in this style (check with me if you're not sure)---discuss in what sense it can be characterized as a reasonable specification language (in addition to whatever programming language properties it possesses). Alternatively, argue why it is a lousy specification language.
Assess Spivey's birthday book example in terms of Michael Jackson's discussion of requirements (the world), programs (the machine), and specifications (their intersection). (I will distribute the introduction of Spivey's book, The Z Notation: A Reference Manual, on Wednesday; this chapter contains this example.)
Capture the essence of the birthday book example using algebraic specifications. (A paper on the approach will be provided next week.)
Harel's paper, "On Visual Formalisms", lays out the basic notion of hierarchical finite state machines, in particular statecharts.
Write a statecharts description for either of the following two devices: the microwave oven on the fourth floor of Sieg Hall, or the touch panel display in any of the classrooms in EE1. You needn't model every aspect of these systems, but list what you didn't model and why. Furthermore, do not worry about precise details of the statecharts definition; they shouldn't be material to this assignment. Finally, I doubt you'll want to do this in softcopy (well, perhaps using something like Visio), so feel free to turn in hardcopy or to scan in your answer.
In one or two paragraphs, argue whether you believe hierarchical state machines must be represented visually to provide maximal leverage, or whether a textual representation would be as useful.