Com S 641/Refinement Calculus Seminar

Resources

This page provides information on some of the resources available for students in Com S 641. The page is organized as follows:

1. Miscellaneous Resources: about the course, refinement calculus, formal methods for Java, and formal methods in general.
2. Reserve List: A list of materials on reserve at the Parks Library

Miscellaneous Resources

The following are some links to various resources you may find useful about the course, refinement calculus, formal methods for Java, and formal methods in general.

Course Resources

• The course documentation directory, including:
  • Errata for the Back and von Wright book.
  • errata for Cohen's book.
• Meeting outlines directory, containing outline files for the "lectures".
• Lecture notes directory, containing strangely formatted notes for the "lectures". We recommend that students use the meeting outlines (above) instead.

Refinement Calculus

• Review of chapter one of the Back and von Wright book by Jeff Thomson
• Programming from Specifications Second Edition (Prentice-Hall International, 1998) by Carroll Morgan. Note that the entire book is on-line.
• Refinement Calculus Tutorial by Michael Butler
• The Programming Methodology Group's web page at Åbo Akademi University including:
  • Ralph-Johan Back
  • Joakim von Wright
• Eric C. R. Hehner
• A tool for formal refinement

Related to homework projects, you might want to look at the following.

• An OO refinement calculus for Eiffel by Richard Paige and Jonathan S. Ostroff
• Mark Utting's Ph.D. thesis on OO refinement calculus.
• The Structure of Typed Programming Languages by David A. Schmidt (MIT Press, 1994).
• Emil Sekerinski's paper on type theory for OO refinement calculus

Formal Methods for Java

• The Java modeling language (JML) home page.
• Extended Static Checking project at Compaq Systems Research Center.
• LOOP project from Bart Jacobs's group in Nijmegen.
• iContract, which supports specifications in javadoc comments.
• iDoclet, the iContract doclet.
• The Jass tool, which supports design by contract for Java.
• The Infospheres Java Coding Standard.
• Doclets written in Javadoc, some of which pertain to specification.
• DowWiz - The JavaDoc Documentation Tool.
• JUnit for Java test cases.
• Java PathFinder a model checker for Java programs.
• Bandera a model checker and model checking framework for Java programs.
• Mocha model checker home page.
• Daikon dynamic invariant detector.
• Hyper/J, a tool supporting "multi-dimensional separation of concerns" for Java.
• AspectJ, aspect-oriented programming for Java.
• Other Java tools.

Other Formal Methods Resources

• The World-Wide Web Virtual Library: Formal Methods.
• The SETS calculus
• Abstract State Machines
• The Risks Digest: Forum On Risks To The Public In Computers And Related Systems and Illustrative Risks to the Public in the Use of Computer Systems and Related Technology.
• Alloy Constraint Analyzer, an object modeling notation and lightweight formal method.
• OCL page, of links concerning the Object Constraint Language.
• The Larch FAQ.
• IFAD's site for VDM-SL and related tools.
• Eiffel
• Gary Leavens's favorite formal method links.

Return to top

Reserve List

To check out one of these (for a few hours or days), go to the Parks library reserve desk. Take along the call number and title, or look up Com S 641 there.

Required Text

Required

Other Texts On Calculation, Verification, and Refinement

Return to top

Last modified Tuesday, January 22, 2002.