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.

翻译：正确性可构造（CbC）是一种增量式程序构建过程，用于构造功能正确的程序。程序在构建过程中逐步完善并附带规范，该规范本质上保证了其被满足。由于CbC需要在编程语言基础上额外添加一组固定粒度的预定义精化规则，没有专用工具支持时难以使用。每条精化规则引入特定的编程语句，开发者无法偏离这些规则来构造程序。CbC允许以结构化和增量式的方式开发软件以确保正确性，但灵活性有限是其不足之处。本研究比较了经典CbC与CbC-Block和TraitCbC两种方法。CbC-Block和TraitCbC均与CbC相关，但它们引入了新的语言构造，支持更灵活的软件构造方式。我们为这两种方法提供了编程指南，与CbC类似，该指南可引导生成结构良好的程序。CbC-Block通过增加一条插入任意语句块的精化规则来扩展CbC，因此我们将CbC-Block作为CbC的扩展进行介绍。TraitCbC基于具有指定方法的特质（traits）实现正确性可构造。我们形式化地引入了TraitCbC，并证明了构造策略的可靠性。本文从编程构造、工具支持和可用性三个方面对三种开发方法进行了定性比较，以评估其各自最适合的任务类型与开发者群体。