Formalisation is good.
Look at notation (Alloy).
Specification. What not how.
- State based (derived from Z).
- Hoare-style (huh?!). He put this in brackets, maybe it wont be in the exam.
Refinement. How, linked to what.
- Data-refinement; forward and backward (also known as upward and downward).
- These are tests expressed as predicates which show how the ‘how’ meets the ‘what’ we defined previously.
Miscellany. – Looking at other notations other than Alloy, also sounds a bit unnecessary.
‘What is there to learn?’
- Understand the concepts behind state-based and trace-based specifications.
- Meet the syntax specified for state-based and trace-based specifications (e.g. variable names such as t_in).
- Learn forward and backward data-refinement rules.
- 10 marks.
- Alloy notation.
Question 2, 3, 4
20 marks each.
- Construct a state-based specification.
- Understand and convert state-based specifications: Explaining how the Alloy works, looking at the pre-conditions, converting state-based to trace-based.
- Refinement, based around state-based style. Previous exams were apparently over-generous somewhere or another. Previously it was 10-10 but this time might be 13-7. Something like that.