Comparing correctness-by-construction with post-hoc verification—a qualitative user study

Tobias Runge, Thomas Thüm, Loek Cleophas, Ina Schaefer, Bruce W. Watson

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

Correctness-by-construction (CbC) is a refinement-based methodology to incrementally create formally correct programs. Programs are constructed using refinement rules which guarantee that the resulting implementation is correct with respect to a pre-/postcondition specification. In contrast, with post-hoc verification (PhV) a specification and a program are created, and afterwards verified that the program satisfies the specification. In the literature, both methods are discussed with specific advantages and disadvantages. By letting participants construct and verify programs using CbC and PhV in a controlled experiment, we analyzed the claims in the literature. We evaluated defects in intermediate code snapshots and discovered a trial-and-error construction process to alter code and specification. The participants appreciated the good feedback of CbC and state that CbC is better than PhV in helping to find defects. Nevertheless, some defects in the constructed programs with CbC indicate that the participants need more time to adapt the CbC process.

Original languageEnglish
Title of host publicationFormal Methods. FM 2019 International Workshops - Revised Selected Papers
EditorsEmil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, David Delmas
Place of PublicationCham
PublisherSpringer
Pages388-405
Number of pages18
ISBN (Electronic)978-3-030-54997-8
ISBN (Print)978-3-030-54996-1
DOIs
Publication statusPublished - 2020
Event3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Duration: 7 Oct 201911 Oct 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12233 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd World Congress on Formal Methods, FM 2019
CountryPortugal
CityPorto
Period7/10/1911/10/19

Fingerprint Dive into the research topics of 'Comparing correctness-by-construction with post-hoc verification—a qualitative user study'. Together they form a unique fingerprint.

Cite this