论文标题
正确构造编程的特征
Traits for Correct-by-Construction Programming
论文作者
论文摘要
我们证明，在存在传统事后验证（PHV）的情况下，在现有的编程语言中支持正确性（CBC）的自然方式。通过按构造正确性，程序将逐步构建，并固有地保证可以满足的规范。无需专门的工具支持即可使用CBC，因为它需要一组固定粒度的完善规则，这是编程语言之上的其他规则。 在这项工作中，我们提出了TraitCBC，这是一种增量程序构建程序，该程序通过使用特征根据PHV实现正确性。 TraitCBC可以通过特质组成而不是改进规则来构建程序。它提供了一个与CBC类似的编程指南，应导致结构良好的程序，并允许灵活地重复使用经过验证的程序构建块。我们正式介绍了TraitcBC，并证明了我们的验证策略的健全性。此外，我们实施了属性属性作为概念证明。
We demonstrate that traits are a natural way to support correctness-by-construction (CbC) in an existing programming language in the presence of traditional post-hoc verification (PhV). With Correctness-by-Construction, programs are constructed incrementally 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 refinement rules of fixed granularity which are additional rules on top of the programming language. In this work, we propose TraitCbC, an incremental program construction procedure that implements correctness-by-construction on the basis of PhV by using traits. TraitCbC enables program construction by trait composition instead of refinement rules. It provides a programming guideline, which similar to CbC should lead to well-structured programs, and allows flexible reuse of verified program building blocks. We introduce TraitCbC formally and prove the soundness of our verification strategy. Additionally, we implement TraitCbC as a proof of concept.
