Flexible Correct-By-Construction Programming
Date
2023
Authors
Runge, Tobias
Bordis, Tabea
Potanin, Alex
Thum, Thomas
Schaefer, Ina
Journal Title
Journal ISSN
Volume Title
Publisher
International Federation of Computational Logic (IfCoLog)
Abstract
Correctness-by-Construction (CbC) is an incremental program construction process to construct functionally correct programs. The programs are constructed stepwise along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of predefined refinement rules of fixed granularity which are additional rules on top of the programming language. Each refinement rule introduces a specific programming statement and developers cannot depart from these rules to construct programs. CbC allows to develop software in a structured and incremental way to ensure correctness, but the limited flexibility is a disadvantage of CbC. In this work, we compare classic CbC with CbC-Block and Trait-CbC. Both approaches CbC-Block and Trait-CbC, are related to CbC, but they have new language constructs that enable a more flexible software construction approach. We provide for both approaches a programming guideline, which similar to CbC, leads to well-structured programs. CbC-Block extends CbC by adding a refinement rule to insert any block of statements. Therefore, we introduce CbC-Block as an extension of CbC. Trait-CbC implements correctness-by-construction on the basis of traits with specified methods. We formally introduce Trait-CbC and prove soundness of the construction strategy. All three development approaches are qualitatively compared regarding their programming constructs, tool support, and usability to assess which is best suited for certain tasks and developers.
Description
This work was partially supported by funding from the topic Engineering Secure Systems of the Helmholtz Association (HGF) and by KASTEL Security Research Labs (46.23.03). We thank Frederik Fr¨oling for his work on CbC-Block in his Master’s Thesis.
Keywords
Traits, Correctness-by-Construction, Formal Methods, Post-hoc Verification
Citation
Collections
Source
Logical Methods in Computer Science
Type
Journal article
Book Title
Entity type
Access Statement
Open Access
License Rights
Creative Commons Attribution licence
Restricted until
Downloads
File
Description