編譯與模塊細化

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。除此之外，這意味着它們不會被編譯，所以你不會得到那個錯誤。

經過這兩個小小的更改，文件的其餘部分編譯正確。