灵活、按建筑逐项调整的方案拟订 (Flexible Correct-by-Construction Programming)

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 和 Cb- Block 和 TraitCBC 之间有着内在的保障。校正 CbC 与 CbC- Block 和 TraitCBC 相比,使用起来很复杂, 不需要专门的工具支持。 CbC- Block 和 TraitC 两者都与 CbC 相关, 但是它们都有新的语言结构, 使得软件构建方法更加灵活。我们为两种方法提供了一种与 CbC 相似的编程指南, 导致程序结构完善。 Cb- Clock 扩展 Cb C, 通过添加一个精细化规则, 插入 Cnality C 和 Crality C 的校正 C 方法。因此, 我们引入了 C- bralC 的C 系统构建方法。

相关内容