Testing, Debugging and Verification - Formal Specification, part 3

Testing, Debugging, and Verification	TDA566/DIT082, LP2, HT2011
Lecture Notes, November 22.
Topics This lecture continues the introduction of JML. It discusses: First-Order in Specifications Result Values Data Constraints JML Invariants Exceptional Method Behavior Allowing Non-Termination JML Modifiers II Inheritance Slides FormalSpecification3.pdf FormalSpecification3-handout.pdf Examples FormalSpecification3_Examples.zip Reading hints For an introduction into JML, we refer to our book Verification of Object-Oriented Software: The KeY Approach. You can access, and download, the online version from a Chalmers account. See chapter 5 'Formal Specification'. The sections 5.1 to 5.3 are sufficient for our purpose. See also the JML papers at the links page.

Home \| Course \| Schedule \| Exam \| Exercises \| Labs \| Evaluation \| Tools \| Links	W. Ahrendt, V. Klebanov, Nov 18, 2011