在Dafny中形式化Omega测试
Formalizing the Omega Test in Dafny
- Alexandru Ioan Cuza University of Iași（亚历山德鲁·约安·库扎大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本研究在Dafny中完成了用于判定不等式系统可满足性的Omega测试的形式化，定义了相关约束的可执行表示与语义解释，完成了完整规范与验证，并总结了形式化过程带来的经验与新见解。
AI中文摘要：
我们提出了Omega测试在Dafny中的形式化实现，Omega测试是一种用于判定不等式系统可满足性的算法。该实现定义了有理数、线性表达式、不等式、等式、可分性约束和约束系统的可执行表示，以及它们通过赋值得到的语义解释。我们在Dafny中对该实现进行了完整的规范说明与验证。我们描述了所得的经验教训，以及形式化过程如何带来对该算法的新见解。
英文摘要：
We present a formalization in Dafny of the Omega Test, an algorithm used to decide the satisfiability of a system of inequalities. The implementation defines executable representations for rational numbers, linear expressions, inequalities, equalities, divisibility constraints, and systems of constraints, together with their semantic interpretation through valuations. We fully specify and verify the implementation in Dafny. We describe the lessons learned and how the formalization process led to new insights into the algorithm.
