1. Formalisation is good.

2. Look at notation (Alloy).

3. Specification. What not how.

   • State based (derived from Z).
   • Trace-based.
   • Hoare-style (huh?!). He put this in brackets, maybe it wont be in the exam.

4. Refinement. How, linked to what.

   • Data-refinement; forward and backward (also known as upward and downward).
   • Implication.
   • These are tests expressed as predicates which show how the ‘how’ meets the ‘what’ we defined previously.

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

Examination Rubric

Question 1

• 10 marks.
• Alloy notation.

Question 2, 3, 4

• 20 marks each.

• Choose 2.

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