用于对称属性的霍尔逻辑（A Hoare Logic for Symmetry Properties）

《Proceedings of the ACM on Programming Languages》：A Hoare Logic for Symmetry Properties

自然程序正确性性质可通过对称性表达，但现有形式化方法支持不足。本文设计了一种形式化群作用的语法，开发了Hoare-style验证逻辑，并构建原型工具SymVerif验证对称性属性，成功发现McLachlan与Quispel动态系统模型的错误。

　　

摘要

许多自然程序正确性属性可以通过对称性来表述，但现有的形式化方法在推理这些属性方面支持甚少。我们研究了如何形式化验证用群作用表达的广泛对称性属性。为了指定这些属性，我们设计了一种群作用的语法，支持标准的构造和一种自然的蕴含概念。接着，我们开发了一种Hoare风格的逻辑来验证命令式程序的对称性属性，在这种逻辑中，群作用替代了典型的前置条件和后置条件断言。最后，我们开发了一个原型工具SymVerif，并使用它来验证一系列手工制作的基准测试案例中的对称性属性。我们的工具发现了一个由McLachlan和Quispel在[Acta Numerica 2002]中描述的动态系统模型中的错误。