1

我正在尝试 TLA+ 的定理证明工具来证明算法的安全性。但我发现 TLAPS 无法计算出非常“简单”的数学事实。

我的第一个问题是：

EXTENDS Naturals
CONSTANTS x,y
ASSUME x \in Nat /\ y \in Nat
LEMMA x=y+1 => y<x
  OBVIOUS

TLAPS 不能单独使用任何后端证明者来完成。我还尝试使用特定的后端证明者和其他策略：

LEMMA x=y+1 => y<x
  BY IsaM("blast")

但也失败了。类似地，不能检查其他类型的简单事实，例如：

LEMMA x<y => x<y+0

我过去使用过一些后端定理证明器，例如 Z Solver 或 Isabelle，据我所知，它们非常强大。我想我在这里遗漏了一些东西......或者我不理解 TLAPS 证明组织者，或者我仍然需要加载一些带有公理的其他模块？

4

1 回答 1

2

看来您在 TLAPM 中遇到了一个错误——至少在我机器上的开发版本中是这样。原因是 SMT 翻译没有采用第二个假设。没有域限制，任何断言都不应该是可证明的。作为热修复，我将域限制添加到本地引理。我现在可以证明：

LEMMA ASSUME x \in Nat, y \in Nat
      PROVE x=y+1 => y < x BY SMT

目前绕过它的另一种方法是命名假设，在需要时调用它们：

ASSUME DOM == x \in Nat /\ y \in Nat
LEMMA x=y+1 => y < x BY SMT, DOM

应该通过。在这两种情况下，您都必须EXTENDS TLAPS在规范的开头添加以启用SMT关键字。

我还将向维护人员报告该错误。

更新：似乎 TLAPM 通常忽略了全局假设（出于性能原因，afaik）。带有命名假设的版本是首选方法。

于 2019-05-28T17:18:14.580 回答