[VAK 03-604.06] Specification and Verification of Java Programs

In modern software development, the formal verification of program correctness plays an increasingly important role. This course is concerned with the specification and verification of object-oriented programs in Java, with particular emphasis on the Java Modeling Language (JML), which serves in particular for design level specification. There are various verification tools for JML, such as the Extended Static Checker (ESC/Java), the application of which will form a central part of the course work.

• Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. Draft tutorial.
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Kluwer, 1999.

Course Material

• Slides on the syntax and semantics of IMP
• Slides on the syntax and semantics of Hoare Triples
• Slides on Hoare logic rules
• Problem sheet 1 (includes hint for exercise b)
• Slides on Hoare rules for total correctness
• Slides on exceptions
• Problem sheet 2
• Design by contract with JML
• Introduction to JML
• Esc/Java 2 - Use and features
• ESC/Java2 warnings
• Specification tips and pitfalls
• Advanced JML
• Model types  Example: priority queues
• Exercise for May 18th: specify the problems of exercise sheet 1 and 2 in JML (omit the catch-clause in exercise 3 of sheet 2)
• Problem sheet 3 Array.java
• Problem sheet 4 Queue.java