Functions to appear outside of annotations

user_17671161 0
Viewed 47

I am going through the Dafny online tutorial (https://dafny-lang.github.io/dafny/OnlineTutorial/guide). Right after Exercise, it mentioned that functions can only appear in annotations. Thus, one cannot write:

var v := abs(3);

The tutorial also mentioned that sometimes it is convenient to use a function in real code, so one can define a function method, which can be called from real code.

So in Exercise 5, this is what I have written:

function max(a: int, b: int): int
{
   if a < b then b else a
}
method Testing() {
    var a := 3;
    var b := 4;
    var c := max(a,b); //seems like Dafny accept this program as oppose what was said in the tutorial
    assert a <= c && b <= c;
}

I was expecting an error at the line

var c := max(a,b);

However, I didnt get any error.

On the other hand, in Exercise 6, when I have the following as code:

function abs(x: int): int
{
   if x < 0 then -x else x
}
method Abs(x: int) returns (y: int)
    ensures y == abs(x);
{
   y := abs(x);
}

I have the error at the line:

y := abs(x);

stating that "function calls are allowed only in specification contexts (consider declaring the function a 'function method')".

After I changed the line function abs(x: int): int to function method abs(x: int): int, then the error is gone.

May I check why does it work in Exercise 5 but not in Exercise 6?

Anyway, may I also check what does it mean when they use the term "real code" in the phrase "to use a function in read code"?

Thank you.

dafny
1 Answers

The tutorial is slightly out of date. Thank you for reporting it. I have filed an issue on GitHub to update the tutorial and fix this.

Here is an explanation of what's going on.

As you have learned in the tutorial, Dafny makes a strong distinction between "specification contexts" (such as requires/ensures clauses, assert statements, and other annotations) and "real code" (any method that is not declared ghost). Certain features of Dafny are only available in specification contexts.

In older versions of Dafny, the user had to explicitly declare each variable to be ghost in a method if they wanted that variable to have access to specification-context-only features.

In modern Dafny, if the right-hand side of a variable assignment requires a specification context, then the variable is automatically declared ghost.

Thus, in Exercise 5, the code works fine because c is automatically declared ghost by Dafny. Since c is only used inside an assertion, everything is fine.

In Exercise 6, you are trying to return abs from the method. This is not inside an annotation but is instead "real code". (We might want to compile and run it!) Since y is the return parameter for Abs, it is not a ghost variable, since its value must exist at run time. So when you assign y := abs(x), the right-hand side of the assignment is in a "real code" context, where it is not allowed to call functions like abs.

The fix for Exercise 6 is to declare abs a function method.

user_4382670
Related