Description

One of the key concepts in formal specification and verification is modularisation. This means that methods are specified and verified in separation, and then are used as modules in other verification tasks. Whenever some method is called in the verified source code, or referenced in the specification itself (a common practice with query or getter methods) the method specification is used as a formal description of its behaviour and applied in the correctness proof, rather than relying on the methods source implementation. This technique of proving programs correct is especially important in the context of library methods, i.e. the APIs, that are commonly reused in many programs. In some cases (e.g. proprietary APIs), the source of library implementation is not available at all, in which case the formal specification is the only artefact that can be employed in a correctness proof. The lack of good quality API specifications is a weak point of many modern verification tools.

The setting for this work is the VerCors project, where Java concurrent data structures are to be verified. There specifications are written in a mixture of the Java Modelling Language (JML) and concurrent separation logic with permissions. In the scope of the VerCors work also the sequential collection classes from the java.util package need to be specified in the separation logic style, as they are often referenced in the concurrency package  specifications.

An alternative for this work (can be done in parallel by a different person, or the two efforts can be combined in a team work of two) is to specify the same Java collection classes in JML* for the KeY verification system. JML* is a KeY specific extension of JML that enables dynamic frames style specifications. The KeY system is also going to be used in the VerCors project at a later stage. As KeY is a fully functional verification system, for this task the additional effort will be to verify parts of the Java collections source implementation with KeY.

A work-in-progress version of regular JML specifications for the collection classes in the java.util package is available in the OpenJML tool suite distribution. This can be used a starting reference point for this MSc work. Also, there is a minor thesis entitled "Specifying selected parts of the Java API using Dynamic Frames" (the text is available from W. Mostowski on request) that was done in the context of the KeY system. This is a good reference and starting point for this project too.

The specific tasks in this projects would be:

• literature study,
• careful identification of java.util classes and interfaces to be specified, including the order and dependencies of the selected classes,
• using the chosen formalism, specification of the selected classes,
• evaluation of the specifications. For the separation logic this would be done with the current version of the VerCors tool and/or possibly by manual correctness proofs of the API implementation. For the dynamic frames specifications the evaluation should be done with the KeY system by verifying parts of the API implementation,
• overall evaluation of the work and the tools.

References and bootstrap reading:

1. A. Amighi, S. Blom, M. Huisman, M. Zaharieva-Stojanovski. The VerCors Project. Setting Up Basecamp. In proceedings of Programming Languages meets Program Verification (PLPV 2012).
   http://wwwhome.ewi.utwente.nl/~marieke/vercors-basecamp.pdf
2. Clément Hurlin. Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis, Université Nice - Sophia Antipolis, September 2009.
   http://tel.archives-ouvertes.fr/docs/00/42/49/79/PDF/these-clement-hurlin.pdf
3. Gary T. Leavens, Joseph R. Kiniry, and Erik Poll. A JML tutorial: Modular specification and verification of functional behavior for Java. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification 2007, LNCS 4590, Springer 2007.
   http://sourceforge.net/apps/trac/jmlspecs/export/2547/TeachingMaterials/trunk/CAV2007Tutorial/JMLTutorialPresentation.pdf
4. W. Mostowski. Formal Specifications for Java Real-time Libraries. CHARTER project deliverable D6.2.
   http://wwwhome.ewi.utwente.nl/~mostowskiwi/papers/RealtimeJavaAPISpecs_D6.2.pdf
5. OpenJML: http://sourceforge.net/apps/trac/jmlspecs/wiki/OpenJml
6. B. Weiß. Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. [Primarly Chapter 2 & 3 on JML and JML*.]
   http://digbib.ubka.uni-karlsruhe.de/volltexte/documents/1600837
7. KeY project and tool. http://www.key-project.org