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

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