• Hoare-style buffer correctness (PDF)
• Object-Z: scene 1 (PDF)
• Object-Z: scene 2 (PDF)
• Logic programs as speecifications (PDF)