Supplementary Information for COMP31111


  • Course plan
  • Practical work
  • Course slides
  • General resources

    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.

    Course Plan

    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.
    Overall Course Assessment.
    Assessed Exercises: 20%
    Exam: 80%

    Course Slides

    Course Slides (.pdf)

    Practical Work

    COMP31111 Exercises (.pdf)

    Course Examples Sources

    Perfect Developer Examples (.zip)

    Exercise Sources (.zip)

    General Resources

    Escher Technologies Homepage
    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)

    Some Books

    Habrias H, Frappier M. (eds.)
    Software Specification Methods
    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.)

    Past Papers

    Past Papers (.pdf)