If you get compiler errors like these, the issue is essentially that you haven't provided the whole program yet. The simplest way to solve this problem is to replace "type G" with a concrete type declaration (like "class G { }" or "datatype
G = GConstructor") and to give a body for each function and method. However, this may not always be the most elegant solution, especially if what you're trying to convey with your program text is that your verification is parametric in the type/function/method.
Let me illustrate.
Suppose you have a program with a method "M" that works with any integer function "f", provided "f" is monotonic. Like this one:
function f(x: int): int
lemma Monotonicity(x: int, y: int)
ensures x <= y ==> f(x) <= f(y);
method M(s: int, t: int) returns (r: int)
requires f(s) <= t;
ensures f(r) <= t;
{
Monotonicity(s - 5, s);
r := s - 5;
}
Here, function f is not given any body, since the intention is to prove the rest of the program independent of what that body is. And since the lemma is not given a body, it is never proved, which means that it really acts as an axiom. This program verifies.
When you compile it, the function and lemma, which are ghost, would be erased. However, the compiler will complain, because "f" and "Monotonicity" have not been given bodies.
Here are three options Dafny gives you to get a compiling program.
One option is, as I mentioned above, to just give the bodies of the function and lemma. For example:
function f(x: int): int
{
x + 13
}
lemma Monotonicity(x: int, y: int)
ensures x <= y ==> f(x) <= f(y);
{
}
method M(s: int, t: int) returns (r: int)
requires f(s) <= t;
ensures f(r) <= t;
{
Monotonicity(s - 5, s);
r := s - 5;
}
The presence of the body of the lemma causes Dafny to verify the postcondition, which on behalf of the given function definition goes through automatically. This option is not quite satisfactory, though, because the function definition is also available to
method M. Hence, we don't know if method M is correct for any monotonic function or if M is correct only for this one given function.
Another option is to declare function "f" as "opaque" (this is a new feature in Dafny). A function being opaque means that its defining body will not be used except in places where the program chooses to reveal the definition, which for
opaque functions is done using the automatically generated lemma reveal_f():
function {:opaque} f(x: int): int
{
x + 13
}
lemma Monotonicity(x: int, y: int)
ensures x <= y ==> f(x) <= f(y);
{
reveal_f();
}
method M(s: int, t: int) returns (r: int)
requires f(s) <= t;
ensures f(r) <= t;
{
Monotonicity(s - 5, s);
r := s - 5;
}
Here, the Monotonicity lemma verifies only if you call the lemma that reveals the definition of f. Since method M does not directly reveal f, we know that it is independent of the precise definition of f, so long as the monotonicity property holds.
The third option involves modules. First, put the original declarations into a module, say A. In module A, f is uninterpreted, the Monotonicity lemma is unproved, and method M is verified with just that information:
abstract module A {
function f(x: int): int
lemma Monotonicity(x: int, y: int)
ensures x <= y ==> f(x) <= f(y);
method M(s: int, t: int) returns (r: int)
requires f(s) <= t;
ensures f(r) <= t;
{
Monotonicity(s - 5, s);
r := s - 5;
}
}
Note that I declared the module as "abstract", which tells the compiler not to generate any code for it and to forgive (or, rather, to postpone--compare with the "eat me when I'm fatter" plot of "The Three Billy Goats Gruff" :))
these kinds of compilation errors. Then, declare a refinement module, say B, of A:
module B refines A {
function f...
{
x + 13
}
lemma Monotonicity...
{
}
}
The two occurrences of "..." (which is concrete syntax in Dafny) indicate that the function and lemma have the respective signatures from the refined module but will be further defined here. (In the Dafny IDE in Visual Studio, you can place the mouse
of the "...", which gives you a hover text telling you what omitted information is being inherited from the refined module.) In particular, module B gives bodies to both "f" and "Monotonicity". This means that B gets charged with
the proof obligation to establish lemma Monotonicity's postcondition (in other words, converting the axiom to a theorem). Method M remains the same as in module A (and, in fact, Dafny has the smarts to realize that M does not need to be re-verified in B since
the responsibility for M's correctness lies with A).
Rustan