Trace-Based Specifications

These are lecture notes from my Computer Science course. For learning about formal specifications of systems, I recommend Software Abstractions: Logic, Language, and Analysis.

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…

This entry was posted in fss, lecture. Bookmark the permalink.