The verification is a typical example of a modular verification, where small parts of the program are verified in isolation, assuming the correctness of the other parts. Typical problems that occur in such verifications are discussed.
Specifications of the classes involved in the verification are presented (using the Java Modeling Language (JML) as a specificiation language), and finally it is shown that the implementation satisfy this specification.
Back to schedule.