SPLASH 2020 (series) / ECOOP 2020 (series) / FTfJP 2020 (series) / Formal Techniques for Java-like Programs /
History-based Specification and Verification of Java Collections in KeY
The main topic of this lecture is a discussion of how to reason about Java interfaces with a particular application to Java’s Collection interface. A new specification method (in the state-of-the-art theorem prover KeY) will be introduced which uses histories that record method invocations and their parameters on an interface. To be discussed are the challenges of proving client code correct with respect to arbitrary implementations, and a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).