Testing, Debugging, and Verification TDA566/DIT082, LP2, HT2011
Lecture Notes, November 16.

Topics

In this lecture, we round up the subject of First-Order Logic, and start with JML.
  • in First-Order Logic, we introduce briefly semantic notions, and list some useful valid formulas
  • in JML, we introduce the most common constructs, including pre-/post-conditions, assignable clauses, additional modifiers, JML expressions, and first-order logic in specifications.

Slides

Reading hints

For learning more about First-Order Logic, 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. Chapter 2 'First-Order Logic' gives a thorough account on the topic. The sections 2.2 to 2.4.2 are more than sufficient for our purpose.


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