Compiling Abstract Modules

Apr 11, 2014 at 2:37 PM
I have a program with an abstract module, which I then refine to produce a concrete module. I would like to compile such a program, but I cannot because due to the missing bodies in the abstract module. Is there any way to compile such a program?

For example:
module Abstract
{
    static function method inc(x:int) :int
}

module Concrete refines Abstract
{
    static function method inc(x:int) :int
    {
        x + 1
    }
}

method Main()
{
    print Concrete.inc(1);
}
Gives the output:
Dafny program verifier version 1.8.1.10324, Copyright (c) 2003-2014, Microsoft.

Dafny program verifier finished with 4 verified, 0 errors
Compilation error: Function _0_Abstract_Compile._default.inc has no body
Apr 11, 2014 at 8:05 PM
I found the answer. There is an "abstract" keyword for modules that tells Dafny not to produce code for them. write "abstract module" instead of "Module".
Marked as answer by lexicalscope on 4/11/2014 at 12:05 PM