1

我一直在建模任务中使用抽象引理和函数（没有主体）。在这个例子中，

lemma py(c : int) returns (a: int, b :int)
    ensures a*a + b*b == c*c

lemma main(c : int) returns (a: int, b :int)
    ensures a*a + b*b == c*c
{
    a, b := py(c);
}

在 main 中调用 py 可确保后置条件为真，而不管 py 是如何实现的。我有两个问题：

  1. 在 Dafny 中使用抽象引理/函数是否安全？对上述代码的以下修改由 Dafny 验证：

    lemma py(c : int) returns (a: int, b :int)  
    ensures a*a + b*b == c*c  
    ensures a*a + b*b != c*c

    虽然我认为这可能是 Dafny 应该抛出一个错误。

  2. 我应该说lemma {:axiom} py(...)吗？我没有观察到包括{:axiom}or的区别{:imported}。

4

2 回答 2

1

正如 James 所提到的，在对您未实现的行为进行建模时，没有实体的引理可能很有用。如果您不提供正文，则验证者不会尝试验证引理的正确性。因此，它本质上是一个公理。

即使没有/noCheatingJames 提到的标志，Dafny 编译器也会抱怨无体引理（以及方法和函数）。请注意，在验证者满意之前，编译器不会启动。该{:axiom}属性表示您愿意为引理的真实性承担责任。对于无主体的非重影方法，您还可以使用该{:extern}属性，它可以让您链接到用其他语言编写的代码。同样，您对外部代码的正确性承担责任，因为 Dafny 验证器不会检查它。

鲁斯坦

于 2017-10-31T23:35:17.987 回答
0

在对未实现的系统部分进行建模时，没有主体的方法和函数确实很有用。

但是，在为此类方法和函数提供后置条件时必须小心，因为它们会变得可信，并且不会被 Dafny 检查。换句话说，如果它们有后置条件，那么使用没有主体的引理或函数 可能是不安全的。

也就是说，这些方法和函数对于建模来说是必不可少的，因此它们可能不安全的事实并不意味着您不应该使用它们。相反，在写下后置条件时应该格外小心，因为它们不会被检查。

如果您将/noCheating:1标志传递给 Dafny，它将抱怨任何没有具有后置条件的主体的方法或函数，并强制您使用该{:axiom}属性。即使没有通过/noCheating:1，这也很有帮助，只是为了标记后置条件是可信的这一事实。是否通过/noCheating:1或是否使用该属性取决于您。

于 2017-10-29T21:12:57.810 回答