By the time the example is done, there will likely be more than you need to include in Ch 3.  You can use as much of the verbiage as you like, but there's ample room for you to structure and present things as you think is best.  Between what's said in the notes and the test file comments, there's quite a bit of fodder.  Feel entirely free to change, reorder, add, subtract as you see fit.

There is some redundancy between the notes and example comments as well, since I tried to synchronize the two presentations amply.  Again, organize things as you need to.

All of the files are in the directory newer-inputs/ch3-examples/.  The best working index to the testing files is the tests.csh shell script.  It has a line that runs each example, showing the name of the testing file, and the name of the spec files.  E.g., the first test case is

   # Test the comment-only version of the AddUser spec.
   fmsl adduser-basic-tests.fmsl adduser-basic.fmsl userdb-objs.fmsl

Note that the userdb-objs.fmsl file needs to be included, since it defines the referenced objects.  For the most part, the example files are in pairs of the for X.fmsl and X-test.fmsl.

All of the tests in tests.csh work except for the last.  The typechecker and interp are fragile in some places, since not all of the validation call type checking works 100%.  The major problem is what I mentioned before, where non-severe errors still get through to the interpreter, even when type checking fails.

So far all of the examples have validated as expected, except for the use of overloaded ops in one of the examples.  Evidently overloading does not work properly for validation calls, so I just renamed the overloaded ops to eliminate the problem.  I'm actually hoping to find a bug in some piece of logic, to demonstrate the usefulness of validation calls.  I've kept a number of bugs found by students in past years, at least one of which can go in as another example of how validation calls can be useful.

The current sticking point is the following postcondition for FindUser, which blows up for something having to do with stack access:

       (exists (ur in udb) (ur.id = id) and (ur' = ur))
           or
       (not (exists (ur in udb) (ur.id = id)) and (ur' = nil));


I'm going to press on with the example, since I'm going to use it in at least a couple places.  It's gone quite a bit slower than I expected, given the bug fixes along the way.  I'll finish an outline of what's left, and we'll work out a very near-term plan for how much needs to go in Chapter 3.


If you're around tomorrow 8am, we can talk then.  Or at your next convenience.