CSE584 (Winter 2001): Assignment #1
Assigned: 9 January 2001
Due: 30 January 2001
  • See the home page for details about turning in the assignment, the specific time for the due date, the assignment's weight, etc.
  • There is an extra week for doing this first assignment: the later ones will have only two weeks from assigned date to due date.  So don't get too used to this!
  1. Program correctness (40 points, 10 points each)
    1. In the second lecture, using the "right" postcondition for computing the maximum:
             (max = x or max = y) and (max >= x and max >= y), 
      push through the proof of the program with respect to this specification.
    2. Prove the following predicate (you can assume x is an integer):

      {x <> 0} if x < 0 then x := -x else x := x - 1 {x >= 0}
    3. Prove the following predicate, making your loop invariant explicit; assume all variables are integers:

      {y > 0}
        z := x;
        n := y;
        while n > 1 do
          z := z + x;
          n := n - 1
        end
      {z = x * y}
    4. Write a specification for a program that accepts three coefficients A, B and C and solves the quadratic equation Ax2 + Bx + C = 0.
  2.  Z (40 points total)

    Note: you may wish to use some of the Z formatting tools described on the web (for instance, here); if you really want, you can try one of the Z type checking tools also found there.  (I am not requiring either of these, because the overhead of learning them is not fully consistent with the value you get for a small assignment.)

    1. (10 points) Consider the AddBirthday schema (on page 4) in Spivey's BirthdayBook example.  What if the bottom line (birthday' = birthday È {name? |® date?) was replaced by the line: {name? |®date?} Î birthday' ?  This says essentially the same thing: the new entry becomes an element of the updated birthday'.  What's wrong with this reasoning, and what specific problem(s) would this change cause in the specification? 
    2. (10 points) In the BirthdayBook example, dates are left as atomic elements: that is, they have no structure (i.e., they can only be compared for equality).  Write a Z specification for Date that would allow for operations that require additional structure on dates, such as distinguishing earlier and later dates, determining the difference between two dates, and any other operations you wish in this general style.  Do not either choose a concrete representation (such as using two digits to represent the year :-) nor make any decisions that preclude reasonable representations of your Date specifications.
    3. (20 points) Write a Z specification of the following system. Your specification should include sufficient explanatory prose to make it easily readable. 

      A teacher wants to keep a register of students in the class, and to record which students have completed their homework. Specify:

      1. The state space for a register. (Hint: use two sets of students.)

        |---Register-----------------------
        | enrolled: STUDENT
        | completed: STUDENT
        |-------
        | ...
        |--------------------------------

      2. An operation to enroll a new student.
      3. An operation to record that a student (already enrolled in class) has finished the homework.
      4. An operation to enquire whether a student (who must be enrolled) has finished the homework. (The answer is either Yes or No).
      5. A robust version of the system.
      6. (Optional) A (robust) version of the system, assuming that, in addition, at most MAX students can be enrolled in the class. (You should not have to rewrite the whole specification to accomplish this.)
  3. Finite state specifications (40 points)

    Write a statecharts specification of the Yahoo! game checkers.  (You'll have to create a Yahoo! account for this.)   After you go to that page (logging in to Yahoo!, if necessary), you should see a screen with a set of "global game rooms" named things like "Hamster Pit" and "Pelican Palace".  What I want is a specification of the system from the time you enter one of those rooms until you exit it (with the exception of playing the checkers game per se).  When you enter the room, you'll get another screen (an applet, in fact) that has a set of tiles: names, ratings, and table information of the people in the room (note that with at the top of the columns you can sort by the different fields), a little chat room for people in the room, some check boxes (to change to small windows, for instance) and buttons (to create a new table, for instance), and the list of the active tables (including the players at them, for instance).  Your specification should capture all these tiles and their interactions (if any), including creating a table, joining a game, etc.  (You need not handle the "Learn More" button.)  You must handle "Play Now", which creates another screen (applet) with the actual checker game; once in this screen, you need to handle coming and going of players and exiting, but nothing else.  (You can handle other stuff, like booting players, if you want, but it's not required.)  

    No, there isn't a good existing specification to work from.  You will have to experiment some yourself.  You can also read some of the material provided under "Learn More".  I'm sure that there will be some questions about what to include and not include: please use the mailing list, so Tao and I can clarify these questions to the whole class.  Finally, remember to use the structure of statecharts to make this specification more manageable!
  4. Miscellaneous (30 points total, 10 points each)
    1. For question (3) --- the checkers specification --- identify three properties that you would like the specification to have that in principle could be checked with model checking.
    2. Find two great examples of bad English language specifications (like the "shoes must be worn" and "dogs must be carried" example from Jackson).  You can beg, borrow, or steal these, as long as you properly attribute them!
    3. Jackson's videotape discusses "Denial by Prior Knowledge" (the same issue, roughly, is discussed in his book on our reading list, in the section titled "Software Engineering" (starting on p. 188).   Are there any areas in software development that fit his criterion of being both "specialized" and "standardized"?  If so, name one and justify why it fits this criterion.  If not, justify your answer (this is, of course, much harder to do).  Be brief (at most several paragraphs).