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 与 CbC-Block 和 TraitCbC 两种方法。CbC-Block 和 TraitCbC 这两种方法都与 CbC 相关，但它们引入了新的语言构造，使得软件构造方法更加灵活。我们为这两种方法提供了编程指南，类似于 CbC，它们能生成结构良好的程序。CbC-Block 通过添加一条精化规则来插入任意语句块，从而扩展了 CbC。因此，我们将 CbC-Block 作为 CbC 的扩展引入。TraitCbC 基于具有指定方法的特质来实现正确性保证构造。我们正式介绍了 TraitCbC，并证明了其构造策略的可靠性。所有三种开发方法在编程构造、工具支持和可用性方面进行了定性比较，以评估哪种方法更适合特定任务和开发者。