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. |
Perfect Developer Examples (.zip)
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)
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.)