The first part of my talk will about the practice of using JML. I will explain a little about JML and then discuss some examples from the JavaCard API, such as the APDU and JCSystem classes, to illustrate the use of JML.
The second part will be about a more theoretical issue, namely the role of invariants in JML and object-oriented (OO) programs in general. The notion of invariant is very well-known, but the precise meaning of invariants in the verification of OO programs is more complicated that one might expect.
Back to schedule.