Note: Some of the graphical elements of this site are only visible to browsers that support accepted web standards. The content of this site is, however, accessible to any browser or Internet device.
- This page is for the Autumn 2004 term.
- » Contact Details/Activities of Michael Huth
- Spring Exam Review: Please consult the class log book entry for 8 Dec on the 302 course home page contains some questions and solutions that should help you in your preparations for the exam.
- » Schedule
- » Course syllabus
- Coursework: will be on Cate on Monday, 22 November; here are the specifications for its third task.
- Lecture 1 » without and » with overlays; Lecture 2 » without and » with overlays; Lecture 3 without overlays and with overlays; Lecture 4 is based on slides by Yoonsik Cheon, An introduction to JML and design by contract using JML, in PowerPoint; and slides by Erik Poll, Assertions & Design-by-contract using JML; Lecture 5 without and with overlays
- Tutorial 4; please read Section 7 of the paper recommended as reading in Lecture 5 in order to obtain suggested answers,
- Tutorial 3, the snippet of Java code with JML annotations from a real case study, and Suggested Answers,
- Tutorial 2 and its Suggested Answers,
- Tutorial 1 and its Suggested Answers,
- Some recommended links:
- Electronic Purse JML case study
- Preliminary definition of JML
- Java Modelling Language (JML) home page
- MoneyTest.java, IMoney.java, Money.java, MoneyBag.java, MoneyTest.java, MoneyBagTest.java, TestAll.java,
- The JUnit Cookbook and its FAQ
- SPeX, checking strong specifications using an extensible software model checking framework
- JML-Testing-Tools, a JML Specification Animator
- Verification of object-oriented programs with invariants, the basis for most of our lectures
- Errata:
- Notes of Lecture 3: in the definition of unpack, the "=" in "p.committed = false" has to be ":=", i.e. an assignment statement. Similar typos occur in Lecture 2, but they are corrected in the online versions.
- Solutions 1: I forgot to define "object invariant" as, e.g., an integrity constraint on on object's data fields and other data assessible through it.
- Tutorial 1: In 2.2 the expression "amount < 0" should read "amount > 0."
- Class log book:
- 6 Dec: Reviewed Tutorial 3, conducted Lecture 5 and Tutorial 4 on practizing annotations with o.inv and o.committed, and commented on what is expected in each of the three tasks of the course work.
- 29 Nov: Reviewed Tutorial 2, did lecture based on Erik Poll's slides.
- 22 Nov: Did Lecture 2, conducted Tutorial 2, presented sole course work, covered Lecture 3 up to, and including the slide on "Definition of pack".
- 15 Nov: presented syllabus, did Lecture 1, conducted and reviewed Tutorial 1.