• Case study (definitions, state, operations and errors)

• Document preparation (LaTeX tool)

• Z type-checking (ZTC tool)

• Z animation (ZANS tool - explicit specifications)

• Common mistakes

• Further mathematical notation ("bags")

• Advanced schema notation for structuring ("promotion")

• Advanced example

• Refinement towards a program (Birthday Book example)

• Industrial use of formal methods (myths and guidelines)

Practicals and tutorials will accompany the lectures.

Assessment will involve the production, type-checking and partial animation of a small Z specification, including informal commentary and a report.

Further information can be found on-line under: