1

在 Dafny 上， alemma被实现为 a ghost method，因此，它仅对规范有用。

但是，您不能从 a 调用引理ghost field，如下所示：

class A {
    var i: int;
    lemma sum_is_commutative(i: int, j: int)
        ensures i + j == j + i
    {}
}
class B {
    ghost var a: A;
    lemma a_sum_is_commutative(i: int, j: int)
        ensures i + j == j + i
    { a.sum_is_commutative(i, j); }
    method test() {
        // a.sum_is_commutative(3, 2); // <- Cannot use directly this
        a_sum_is_commutative(3, 2);
    }
}

这种行为的理由是什么？如何解决？在内部类中重复引理并利用（通常是调用）其他类的最佳选择是lemma什么？

4

3 回答 3

2

感谢您发现并报告这一点。这是一个错误。我只是推了一个修复它。

鲁斯坦

于 2018-11-28T02:17:07.620 回答
0

我无法评论这种行为的基本原理（如果存在学术问题，我将更新所选答案，而不仅仅是错误或缺乏实施）。

为了解决这个问题，定义在语义上是相同的

class A {
  lemma sum_commutative(i: int, j: int) {}
}

就像

class A {
  static lemma sum_commutative(a: A, i: int, j: int) {}
}

因此，即使您需要访问this实例，您也可以将其作为参数传递，而不是隐式依赖它。

然后，您可以从任何其他类调用您的引理，A.sum_commutative(a, i, j)而不会遇到从非幽灵方法调用幽灵变量的幽灵方法的问题。

于 2018-11-22T18:53:02.897 回答
0

我对 Dafny 不熟悉，但我认为您还需要将您的test方法声明为 ghost 才能在其中使用 ghost 参数。

通常在程序验证框架中，ghost意味着定义将在运行时被删除，此处仅用于证明目的。因此，您的test方法不应包含其定义将被擦除的代码，或者应将其标记为可擦除 ( ghost)。

于 2018-11-21T15:15:50.760 回答