dafny - 编译与模块细化

Question

编译以下代码时：

module Interface {
    function addSome(n: nat): nat
        ensures addSome(n) > n
}

module Mod {
    import A : Interface
    method m() {
        assert 6 <= A.addSome(5);
        print "Test\n";
    }
}

module Implementation refines Interface {
    function addSome(n: nat): nat
        ensures addSome(n) == n + 1
    {
        n + 1
    }
}

module Mod2 refines Mod {
  import A = Implementation
}

method Main() {
    Mod2.m();
}

我得到输出

Dafny program verifier finished with 5 verified, 0 errors
Compilation error: Function _0_Interface_Compile._default.addSome has no body

鉴于Implementation精炼Interface，为什么编译器需要Interface.addSome有一个主体，尤其是当addSomeghost 无论如何不应该参与编译时？

Answer 1

您需要将Interface和都标记Mod为abstract。除此之外，这意味着它们不会被编译，所以你不会得到那个错误。

在这两个小的更改之后，文件的其余部分可以正确编译。