Compilation mit Modul Verfeinerung

Question

Wenn Sie den folgenden Code kompilieren:

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(); 
} 

Ich bekomme die Ausgabe

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

Da Implementation verfeinert Interface, warum der Compiler müssen Interface.addSome einen Körper haben, insbesondere, wenn addSome ist sowieso Geist, also sollte nicht in Kompilierung beteiligt sein?

Answer 1

Sie müssen sowohl als auch Mod als abstract markieren. Unter anderem bedeutet dies, dass sie nicht kompiliert werden, so dass Sie diesen Fehler nicht bekommen.

Nach diesen zwei kleinen Änderungen wird der Rest der Datei korrekt kompiliert.