编译与模块细化

Compilation with module refinement

编译以下代码时:

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 来拥有主体,特别是当 addSome 无论如何都是幽灵时,所以不应该涉及在编译中?

您需要将 InterfaceMod 都标记为 abstract。除其他事项外,这意味着它们不会被编译,因此您不会收到该错误。

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