CODEWITHSUNDEEP
z3verificationinsertion-sortdafny
Amir-Mousavi
Amir-Mousavi

Reputation: 4563

Dafny function, invalid logical expression on while loop

I am new in Dafny and getting some errors that I can not figure it out.

Upvotes: 1

Views: 2836

Answers (1)

Theodore Norvell
Theodore Norvell

Reputation: 16221

The first error is because you are declared a function rather than a method. In Dafny the body of a function is expected to be an expression, not a sequence of statements. So when the parser sees the keyword "while", it realizes something is wrong (since "while" can't be part of a statement) and gives an error message. I'm not sure why the error message refers to a "logical" expression.

Anyway, you can fix this problem by declaring a method rather than a function.

You need a method because you are using an imperative algorithm and not a functional algorithm. It's true that you want a subroutine that computes its output as a function of its input with no side effects. But, in Dafny, you still use a method for this when the way you want to do it involves imperative constructs like assignments and while loops.

The second problem is that input[j := b] is an expression whereas the parser exepected a statement. You can fix this by rewriting input[j := b]; input[j-1 := a]; as input := input[j:=b]; input := input[j-1];.

Unfortunately, that will lead to another problem, which is that, in Dafny, input parameters can't be assigned to. So you are better off making another variable. See below, for how I did that.

method insertionSort(input:seq<int>)
// The next line declares a variable you can assign to.
// It also declares that the final value of this variable is the result
// of the method.
returns( output : seq<int> )
    // No reads clause is needed.
    requires |input|>0
    // In the following I changed "input" to "output" a few places
    ensures perm(output,old(input))
    ensures sortedBetween(output, 0, |output|) // 0 to input.Length = whole input

{
    output := input ;
    // From here on I changed your "input" to "output" most places
    var i := 1;
    while (i < |output|) 
        invariant perm(output,old(input))
        invariant 1 <= i <= |output|
        invariant sortedBetween(output, 0, i)       
        decreases |output|-i
    {
        ...
            output := output[j := b];
            output := output[j-1 := a];
            j := j-1;
        ...
    }
}

By the way, since input parameters can't be changed, wherever you have old(input), you could just use input. They mean the same thing.

Upvotes: 4

Related Questions