compilation errors with parametric type

Feb 4, 2014 at 8:48 AM
I'm trying to use a parametric type G and an undefined (no-body) function key: G -> int.
When I compile (on-line) it detect the following two errors:

Error 1 Arbitrary type ('_module.G') cannot be compiled
Error 2 Function _module._default.key has no body

In MVS my program has not verification errors, nor assumes.

There are other programs in Dafny Test suite using a parametric type and a non-bofy function which compile perfectly.

Do you imagine where is the problem?
Coordinator
Feb 5, 2014 at 12:21 AM
Hi Paqui,

The standard mode of operation for Dafny is to first verify the program and output any error messages. If verification succeeds, the program is compiled and any compilation errors are reported. It seems your program verifies but fails to compile.

Compilation errors can arise because the program uses some features that the verifier does not mind but that the compiler does not know what to do with. These include "assume" statements, which cannot be compiled. These also include functions and methods that have not been given an implementation (you can think of such errors as a variation of the link errors you may get after separate compilation). The type analog of a function/method having no body is the declaration of an uninterpreted type (for example, "type G"); in this case, one could imagine that the compiler would automatically generate some type, but the Dafny compiler does not currently do that.

I will describe how to handle such compilation errors in a subsequent reply. But before doing that, let me answer the question about the difference between your program and the one in the test suite. If you run Dafny from the command line (where the default compilation mode is /compile:1), you will get the same compilation errors for both programs. However, rise4fun.com/dafny does the following (which is the same as /compile:3 does from the command line). If the program verifies and the program contains a Main method, then rise4fun will compile your program and, if that also succeeds, run your program. I think the simple explanation to why your program gives these compilation errors while the one in the test suite does not is that your program has a Main method and the one in the test suite does not.

Rustan
Marked as answer by rustanleino on 2/6/2014 at 4:07 PM
Coordinator
Feb 5, 2014 at 1:03 AM
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
Marked as answer by rustanleino on 2/6/2014 at 4:07 PM