Abstract
Deductive program verification is a post-hoc quality assurance technique following the design-by-contract paradigm where correctness of the program is proven only after it was written. Contrary, correctness-by-construction (CbC) is an incremental program construction technique. Starting with the functional specification, the program’s correctness is guaranteed by application of a small set of refinement rules. Even though CbC is supposed to lead to code with a low defect rate and improve the traceability of errors, it is not widespread. One of the main reasons is insufficient tool support which we addressed with our tool CorC. CorC provides support for CbC-based program construction with the KeY program verifier as backend prover for checking correctness of refinement rule applications. However, CorC was limited to constructing single method bodies restricting its applicability. In this work, we introduce and discuss CorC 2.0, which extends CorC ’s programming model with objects as used in object-oriented programming. We integrate CorC into a development process that allows to use post-hoc verification and CbC interchangeably to construct correct programs, and scale the applicability of CbC on the architectural level in our tool extension ArchiCorC. We developed three object-oriented case studies and evaluated the verification effort and the usability of CorC in comparison to post-hoc verification.
Original language | English |
---|---|
Title of host publication | The Logic of Software. A Tasting Menu of Formal Methods |
Subtitle of host publication | Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday |
Editors | Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Einar Broch Johnsen |
Publisher | Springer |
Pages | 80-104 |
Number of pages | 25 |
ISBN (Electronic) | 978-3-031-08166-8 |
ISBN (Print) | 978-3-031-08165-1 |
DOIs | |
Publication status | Published - 2022 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 13360 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Bibliographical note
Publisher Copyright:© 2022, Springer Nature Switzerland AG.