How much Specification is Enough? Mutation Analysis for Software Contracts
Design-by-contract is a light-weight formal development paradigm, in which object-oriented software is specified with so-called software contracts. Contracts are annotations in the source code that explicitly document intended functional behavior and can be used for verifying correctness of a particular implementation or as test oracles during automatic test case generation. As writing strong specifications is an expensive and error-prone activity due to lack of expertise and tool support, developers are often only willing to write simpler specifications, covering only a fraction of all functional properties. As a consequence, software quality is lowered, or even worse, potential bugs remain undetected during software verification. To give developers a sense of specification coverage, we propose a methodology that considers the degree of incomplete specifications by means of mutation analysis. We consider Java programs annotated with JML and employ the deductive program verifier KeY–2.7.0 to show that this approach is applicable to numerous open-source JML projects from the literature.
Tue 18 MayDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:00
|Methodology for Specification and Verification of High-Level Properties with MetAcsl|
Virgile Robles CEA List, Software Reliability and Security Lab, Nikolai Kosmatov CEA List, Virgile Prevosto CEA Tech List, Louis Rilling DGA Maîtrise de l'Information, Pascale Le Gall CentraleSupelecPre-print Media Attached
|How much Specification is Enough? Mutation Analysis for Software Contracts|
FormaliSE 2021Media Attached