Comparing correctness-by-construction with post-hoc verification—a qualitative user study
| Autor: | Runge, Tobias, Thüm, Thomas, Cleophas, Loek, Schaefer, Ina, Watson, Bruce W., Sekerinski, Emil, Moreira, Nelma, Oliveira, José N., Ratiu, Daniel, Guidotti, Riccardo, Farrell, Marie, Luckcuck, Matt, Marmsoler, Diego, Campos, José, Astarte, Troy, Gonnord, Laure, Cerone, Antonio, Couto, Luis, Dongol, Brijesh, Kutrib, Martin, Monteiro, Pedro, Delmas, David |
|---|---|
| Přispěvatelé: | Software Engineering and Technology |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Correctness
Post hoc Programming language Computer science Process (computing) Contrast (statistics) 020207 software engineering 02 engineering and technology Construct (python library) Data_CODINGANDINFORMATIONTHEORY computer.software_genre Postcondition 0202 electrical engineering electronic engineering information engineering Code (cryptography) 020201 artificial intelligence & image processing State (computer science) computer |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030549961 FM Workshops (2) Formal Methods. FM 2019 International Workshops-Revised Selected Papers, 388-405 STARTPAGE=388;ENDPAGE=405;TITLE=Formal Methods. FM 2019 International Workshops-Revised Selected Papers |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-030-54997-8_25 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|