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 and their parameters 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.

(Talk to be also virtually presented at iFM2020, 18th November 2020. Joint work with: Jinting Bian, Frank de Boer, Stijn de Gouw)