一句话：提出并形式化两种更灵活的构造正确编程方法 CbC-Block 和 TraitCbC，并比较其可用性。
正确性构造（CbC）是一种增量式程序构造方法，可保证程序满足规约。但经典 CbC 依赖固定粒度的精化规则，缺乏灵活性。本文比较经典 CbC 与两种扩展：CbC-Block 和 TraitCbC。CbC-Block 通过增加一条可插入任意语句块的精化规则来扩展 CbC；TraitCbC 则基于带指定方法的 trait 实现 CbC，并为其提供编程指南。作者形式化引入 TraitCbC，并证明其构造策略的可靠性。最后从编程构造、工具支持和可用性三方面对三种方法进行定性比较，以评估它们对不同任务和开发者的适用性。
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.
@article{paperbot2212,
title = {Flexible Correct-by-Construction Programming},
author = {Tobias Runge and Tabea Bordis and Alex Potanin and Thomas Thüm and Ina Schaefer},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 2},
year = {2023},
doi = {10.46298/lmcs-19(2:16)2023}
}