Write a Blog >>
Thu 22 Jun 2017 10:55 - 11:20 at Auditorium, Vertex Building - Specification and Verification Chair(s): Doug Lea

The use of formal contracts has long been advocated as an approach to develop programs that are provably correct. However, the reality is that adoption of contracts has been slow in practice. Despite this, the adoption of lightweight contracts — typically utilising runtime checking — has progressed. In the case of Java, built-in features of the language (e.g. assertions and exceptions) can be used for this. Furthermore, a number of libraries which facilitate contract checking have arisen. In this paper, we catalogue 25 techniques and tools for lightweight contract checking in Java, and present the results of an empirical study looking at a dataset extracted from the 200 most popular projects found on Maven Central, constituting roughly 351,034 KLOC.

We examine (1) the extent to which contracts are used and (2) what kind of contracts are used. We then investigate how contracts are used to safeguard code, and study problems in the context of two types of substitutability that can be guarded by contracts: (3) unsafe evolution of APIs that may break client programs and (4) violations of Liskovs Substitution Principle (LSP) when methods are overridden. We find that: (1) a wide range of techniques and tools are used to represent contracts, and often the same program uses different techniques and tools at the same time; (2) overall, contracts are used less than expected, with significant differences between programs; (3) projects that use contracts continue to do so, and expand the use of contracts as they grow and evolve; and, (4) there are cases where the use of contracts points to unsafe subtyping (violations of LSP) and unsafe evolution.

Thu 22 Jun
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Specification and VerificationECOOP Research Papers at Auditorium, Vertex Building
Chair(s): Doug LeaState University of New York, Oswego
10:30 - 10:55
Talk
Concurrent Data Structures Linked in Time
ECOOP Research Papers
Germán Andrés DelbiancoIMDEA Software Institute, Ilya SergeyUniversity College London, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
Link to publication Media Attached
10:55 - 11:20
Talk
Contracts in the Wild: A Study of Java Programs
ECOOP Research Papers
Jens DietrichMassey University, David J. PearceVictoria University of Wellington, Kamil JezekUniversity of West Bohemia, Pilsen, CZ, Premek BradaUniversity of West Bohemia
Link to publication Pre-print Media Attached
11:20 - 11:45
Talk
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
ECOOP Research Papers
Jan-Oliver KaiserMPI-SWS, Hoang-Hai DangMPI-SWS, Derek DreyerMPI-SWS, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Link to publication Media Attached
11:45 - 12:10
Talk
Promising Compilation to ARMv8 POP
ECOOP Research Papers
Anton PodkopaevSt. Petersburg University, JetBrains, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Link to publication Media Attached