Dafny : 没有主体的引理

Question

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

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 确保 post-条件为真，而不管 py 是如何实现的。我有 2 个问题：

在 Dafny 中使用抽象 lemmas/functions 安全吗？对上述代码进行如下修改，经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 应该抛出的错误。
我应该说lemma {:axiom} py(...)吗？我没有观察到包含 {:axiom} 或 {:imported}.

Answer 1

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

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

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

如果您向 Dafny 传递 /noCheating:1 标志，它会抱怨任何没有主体的方法或函数具有后置条件，并强制您使用 {:axiom} 属性。即使没有通过 /noCheating:1，这也很有用，只是为了标记后置条件是可信的。由您决定是传递 /noCheating:1 还是使用该属性。

Answer 2

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

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

鲁斯坦

Dafny : 没有主体的引理

Dafny : lemmas without bodies

dafny