Flexible Correct-by-Construction Programming

Correctness-by-Construction (CbC) is an incremental program constructionprocess to construct functionally correct programs. The programs areconstructed stepwise along with a specification that is inherently guaranteedto be satisfied. CbC is complex to use without specialized tool support, sinceit needs a set of predefined refinement rules of fixed granularity which areadditional rules on top of the programming language. Each refinement ruleintroduces a specific programming statement and developers cannot depart fromthese rules to construct programs. CbC allows to develop software in astructured and incremental way to ensure correctness, but the limitedflexibility is a disadvantage of CbC. In this work, we compare classic CbC withCbC-Block and TraitCbC. Both approaches CbC-Block and TraitCbC, are related toCbC, but they have new language constructs that enable a more flexible softwareconstruction approach. We provide for both approaches a programming guideline,which similar to CbC, leads to well-structured programs. CbC-Block extends CbCby adding a refinement rule to insert any block of statements. Therefore, weintroduce CbC-Block as an extension of CbC. TraitCbC implementscorrectness-by-construction on the basis of traits with specified methods. Weformally introduce TraitCbC and prove soundness of the construction strategy.All three development approaches are qualitatively compared regarding theirprogramming constructs, tool support, and usability to assess which is bestsuited for certain tasks and developers.Comment: arXiv admin note: text overlap with arXiv:2204.0564