Refinement is a task that sounds a lot like the software engineering practises we learnt about in MSD. It is about deciding when an implementation satisfies a contract. When talking about refinement, we refer to the abstract specification/design and the concrete design/implementation.

Stepwise iteration

Stepwise iteration sounds even more like MSD; it is iterating over specifications and designs until you end up with code.

What’s the difference between design and spec?

• A design has more implementation detail. Instead of talking about sets and relations you might talk about lists and balanced trees.
• A design may resolve some non-determinism. Instead of picking any free identifier the system picks the smallest free identifier.

Alloy

We want to make sure that the behaviour of a concrete design matches the abstract design (Alloy deals with designs, as it’s an implementation of the specification I guess).

In a trace model this is easy, you can just write:

concrete_design implies abstract_design

There are examples, the vending_machine and the trp.

However, it’s more complicated in state-based models because the behaviour is described as a collection of predicates, and a state-based model is ‘non-blocking’ (apparently). There are two different characterisations – forward and backward – when a concrete design simulates an abstract design. Sounds confusing.

But apparently, the key with state-based specifications is to find a retrieve relation that shows how to reconstruct the abstract state from the concrete state (a mapping).