This course gives an introduction to verified system development, in which the verification is supported (behind the scenes mostly) by theorem proving technology. Practical work is based on Perfect Developer from Escher Technologies. Lecture material is partly home-grown, partly taken from slides prepared by Tony Mullins, and partly tutorial material from Escher Technologies.

The practical side of the course has been developed using Perfect Developer version 4.10 specifically. An iso image of an installation CD for this is available from the course lecturer.

There are, as yet, no books dealing specifically with Perfect Developer. Some books dealing with similar technologies, and some related general references, are listed at the end of this web page.

Week No. | Slot 1 | Slot 2 |
---|---|---|

Week 1 | Lecture 1. Introduction | Lecture 2. Overview |

Week 2 | Lecture 3. Refinement Theory I | Lecture 4. Refinement Theory II |

Week 3 | Lecture 5. Refinement Theory III | Lecture 6. Automated Reasoning |

Week 4 | Lecture 7. Perfect Basics | Lecture 8. Perfect Classes |

Week 5 | Lecture 9. Collections | Lecture 10. Examples |

Week 6 | Lecture 11. Relations, Genericity | Practical work |

Week 7 | Lecture 12. Perfect Refinement | Practical work |

Week 8 | Lecture 13. More Refinement, Inheritance | Practical work |

Week 9 | Practical work | Practical work |

Week 10 | Lecture 14. Pefect vs. Set Based | Practical work |

Week 11 | Lecture 15. Meyer's View of the Future | Lecture 16. Meyer's Vision ctd. |

Assessed Exercises: 20%

Exam: 80%

Perfect Developer Examples (.zip)

Perfect Developer Free Edition Download Page (Key Required)

Escher Technologies Educational Support Materials (Many Shadowed Here)

Getting Started with Perfect (.pdf) User Guide (.pdf) Language Reference (.pdf)

Command Line Java Interface (.pdf) Graphical Java Interface (.pdf)

Dictionary Example Slides (.pdf) Dictionary Example Slides (6up .pdf)

Verification Hints and Tips (.pdf)

Verification Conditions (.pdf)

WileyBlackwell; ISBN: 1905209347 (2006)

(A collection of chapters each of which looks at tackling

the same problem using a different specification technology.

Probably the best 'comparison website' for specification

technologies available in book form.)

Harry A.

*Formal Methods Fact File: VDM and Z*

John Wiley & Sons; ISBN: 0471940062 (1996)

(Covers two well established methodologies, VDM and Z, in

reasonable depth. Briefer remarks about other approaches.)

Schneider S.

*The B-Method*

Palgrave Macmillan; ISBN: 033379284X (2001)

(There are many books about the B-Method, which is a

methodology similar in spirit (if not in detail) to Perfect.

This book is a nicely written introduction to B. I wish

there was something similar for Perfect.)

Abrial J-R.

*Modeling in Event-B*

Cambridge University Press; ISBN: 0521895561 (2010)

(Event-B is a more recent, technically simpler, development

of the B-Method approach, based on action refinement. This

is the standard text.)

Derrick J., Boiten E.

*Refinement in Z and Object-Z*

Springer; ISBN: 185233245X (2001)

(A detailed treatment of contract and behavioural refinement

for Z and Object-Z.)

Woodcock J, Davies J.

*Using Z*

Prentice Hall; ISBN: 0139484728 (1996)

(A standard textbook for the Z methodology. Includes a detailed

treatment of refinement for Z.)

de Roever W-P., Engelhardt K.

*Data Refinement: Model-Oriented Proof Methods and their Comparison*

Cambridge University Press; ISBN: 0521641705 (1998)

(A general theoretical treatment of refinement based methods,

leading to an overview of several specific methodologies.)