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.


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 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.