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