适用于构造正确性编程的特征
摘要：通过引入特征，我们展示了在现有编程语言中支持逐步验证（CbC）的正确性是一种自然的方法。通过Construction，程序可以逐步构建，并且在本质上保证满足规范。CbC需要特定的工具支持，因为它需要一组固定粒度的细化规则，这些规则是编程语言之上的附加规则。 在这项工作中，我们提出了TraitCbC，一种基于PhV实现逐步构建的增量程序构建过程，它使用特征来代替细化规则。TraitCbC通过特征组合实现程序构建，提供了类似于CbC的编程指南，可以得到结构良好的程序，并允许灵活地重用验证的程序构建模块。我们正式介绍了TraitCbC，并证明了我们验证策略的正确性。此外，我们还作为概念证明实现了TraitCbC。
作者：Tobias Runge and Alex Potanin and Thomas Th"um and Ina Schaefer
论文ID：2204.05644
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-04-13