编译与模块细化

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有一个组织，特别是当addSome反正是鬼，所以不应该参与编译？

Answer 1

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

经过这两个小小的更改，文件的其余部分编译正确。