Tool Support for Correctness-by-Construction
| dc.contributor.author | Runge, Tobias | |
| dc.contributor.author | Schaefer, Ina | |
| dc.contributor.author | Cleophas, Loek | |
| dc.contributor.author | Thüm, Thomas | |
| dc.contributor.author | Kourie, Derrick | |
| dc.contributor.author | Watson, Bruce W. | |
| dc.contributor.editor | Koziolek, Anne | |
| dc.contributor.editor | Schaefer, Ina | |
| dc.contributor.editor | Seidl, Christoph | |
| dc.date.accessioned | 2020-12-17T11:57:58Z | |
| dc.date.available | 2020-12-17T11:57:58Z | |
| dc.date.issued | 2021 | |
| dc.description.abstract | This work was published in International Conference on Fundamental Approaches to Software Engineering 2019. We tackled a fundamental problem of missing tool support of the correctness-by-construction (CbC) methodology that was proposed by Dijsktra and Hall and revised to a light-weight and more amenable version by Kourie and Watson. Correctness-by-construction (CbC) is an incremental approach to create programs using a set of small, easily applicable refinement rules that guarantee the correctness of the program with regard to its pre- and postcondition specifications. Our goal was to implement a functional and user-friendly IDE, so that developers will adapt to the CbC approach and benefit from its advantages (e.g., defects can be easily tracked through the refinement structure of the program). The tool has a hybrid textual and graphical IDE that programmers can use to refine a specification to a correct implementation. The textual editor fits to programmers that want to stay in their familiar environment, while the graphical editor highlights the refinement structure of the program to give visual feedback if errors occur using KeY as verification backend. The tool was evaluated regarding feasibility and effort to develop correct programs. Here, slight benefits in comparison to a standard verification approach were discovered. | en |
| dc.identifier.doi | 10.18420/SE2021_34 | |
| dc.identifier.isbn | 978-3-88579-704-3 | |
| dc.identifier.pissn | 1617-5468 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/34530 | |
| dc.language.iso | en | |
| dc.publisher | Gesellschaft für Informatik e.V. | |
| dc.relation.ispartof | Software Engineering 2021 | |
| dc.relation.ispartofseries | ecture Notes in Informatics (LNI) - Proceedings, Volume P-310 | |
| dc.subject | correctness-by-construction | |
| dc.subject | tool support | |
| dc.subject | formal methods | |
| dc.subject | verification | |
| dc.title | Tool Support for Correctness-by-Construction | en |
| dc.type | Text/ConferencePaper | |
| gi.citation.endPage | 94 | |
| gi.citation.publisherPlace | Bonn | |
| gi.citation.startPage | 93 | |
| gi.conference.date | 22.-26. Februar 2021 | |
| gi.conference.location | Braunschweig/Virtuell |
Dateien
Originalbündel
1 - 1 von 1
Vorschaubild nicht verfügbar
- Name:
- B1-33.pdf
- Größe:
- 39.65 KB
- Format:
- Adobe Portable Document Format