This assignment is due on Monday May 15, 2000.

1. (40 points) Write a Z version of the natural language specification we looked at in class (given again below).  Important note: you are not obliged to specify low-level details such as ET, Alarm, etc.; instead, you are supposed to specify, at an appropriate (and relatively "high" level) the word- and line-justification problem.  In addition, the absolute details of Z are not critical: I don't expect you to know every operator in Z, for example; feel free to describe what you intend by a given operator, as long as it is plausible.  Here is a copy of the Z reference manual (it's over 100 pages, so you probably don't want to print the whole thing): it includes as the first chapter a more complete version of the famous BirthdayBook problem.  For error handling (the equivalent of Alarm), seriously consider using the basic notion of the schema calculus, as sketched in that first chapter.
   
   The program's input is a stream of characters whose end is signaled with a special end-of-text character, ET. There is exactly one ET character in each input stream. Characters are classified as
   
   --break characters - BL (blank) and NL (new-line);
   --non-break characters - all others except ET;
   --the end-of-text character - ET.
   
   A word is a non-empty sequence of non-break characters. A break is a sequence of one or more break characters. Thus, the input can be viewed as a sequence of words separated by breaks, with possibly leading and trailing breaks, and ending with ET.
   
   The program's output should be the same sequence of words as in the input, with the exception that an oversize word (i.e., a word containing more than MAXPOS characters, where MAXPOS is a positive integer) should cause an error exit from the program (i.e., a variable, Alarm, should have the value TRUE). Up to the point of an error, the program's output should have the following properties:
   
   --A new-line should start only between words and at the beginning of the output text, if any.
   --A break in the input is reduced to a single break character in the output.
   --As many words as possible should be placed on each line (i.e., between successive NL characters).
   --No line may contain more than MAXPOS characters (words and BLs).
   
2. (30 points) Prove the following program's correctness, with some care (a^n is exponentiation).  Separately from the correctness proof, informally sketch a proof of termination.
   

   { a >= 0 and n >= 0 }

   p := 1;

   x := n;

   while x <> 0 do

   begin

     x := x - 1;

     p := p * a;

   end

   { p = a^n }
   

3. (15 points) Sketch how you might capture the notion of procedure call in Hoare-style proofs.
   
4. (35 points) Write a statechart-style specification for some device you can find on campus.  Choices include: the operator console in one of the EE1 classrooms, the microwave oven on the fourth floor of  Sieg Hall, etc.  In addition, write down, precisely although not necessarily in a formal language, at least two properties that must be held by the specification and sketch how you would verify these properties.