First. A neat little Alloy trick

You can use a type of univ -> univ -> SomeSet to make a ‘generic’ function of sorts. See purse.als for an example.

Recap

The most general model has two components. A precondition and a postcondition. You can ‘drop’ bits if you can ‘recover’ them. So far we have covered dropping the precondition and recovering the ‘weakest precondition’. Whatever that means.

A Universal state

Every model can use this universal state. It is:

• a single component, trace, that contains the entire history of calls to the system. Doesn’t have to have timestamps
• A ‘call’ is an ‘event’ (instance) which is the operation name, plus the actual data input and output. You use a signature Event to capture this:
• Define sig State{trace : seq Event}
• Post condition is just ‘append event to trace’ – that’s why we can drop it.
• Something about ‘ignoring the input and output’ too.

The specifications

• The entire model is contained in a single module which may open further modules that contain parts of the description.
• More stuff that was on the slide.

There’s some notes about it at http://www-course.cs.york.ac.uk/fss/abz2010.pdf. Oh, JJ wrote it. Did he invent this then?

Ran through examples of Vending Machines and something else…