Flexible Correct-by-Construction Programming

DOI10.46298/LMCS-19(2:16)2023MaRDI QIDQ6135766zbMATH OpenFDO

Authors Tobias Runge, Alex Potanin, Thomas Thüm, Ina Schaefer

Publication date 26 August 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2211.15261

zbMATH Keywords

correctness-by-constructionformal methodspost-hoc verificationtraits

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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 TraitCbC. Both approaches CbC-Block and TraitCbC, 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. TraitCbC implements correctness-by-construction on the basis of traits with specified methods. We formally introduce TraitCbC 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.

Cites work

• A Deductive Approach to Program Synthesis
• A UTP semantics for \textsf{Circus}
• Applying data refinement for monadic programs to Hopcroft's algorithm
• ArcAngel: a tactic language for refinement
• Dafny: an automatic program verifier for functional correctness
• Data refinement in Isabelle/HOL
• Extending FeatherTrait Java with interfaces
• Feature integration using a feature construct
• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 3995020 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• Invariant based programming: Basic approach and teaching experiences
• Modeling in Event B. System and software engineering.
• Refinement Calculus
• Refinements for free!
• Software engineering and formal methods. 10th international conference, SEFM 2012, Thessaloniki, Greece, October 1--5, 2012. Proceedings
• The correctness-by-construction approach to programming
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Traits: correctness-by-construction for free
• Verification of concurrent systems with VerCors
• Verifying traits: an incremental proof system for fine-grained reuse

This page was built for publication: Flexible Correct-by-Construction Programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135766)