History-Based Specification and Verification of Java Collections in KeY

摘要

In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java's Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations including their parameters and return value, on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).