The Exam Lecture

These are lecture notes from my Computer Science course. For learning about formal specifications of systems, I recommend Software Abstractions: Logic, Language, and Analysis.

  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.
This entry was posted in fss, lecture. Bookmark the permalink.