I am new in Dafny and getting some errors that I can not figure it out.
- in my Dafny program for insertionSort (the code is here), I do not understand why I get an
invalid logical expression
on While loop over variablei
.while (i < |input|)
- in the same code at the swapping part (
input[j := b]; input[j-1 := a];
) also I getexpected method call, found expression
. According to the tutorialinput[j:=b]
is replacing index j of seq input with the value of b
The first error is because you are declared a
function
rather than amethod
. In Dafny the body of afunction
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 afunction
.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 rewritinginput[j := b]; input[j-1 := a];
asinput := 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.
By the way, since input parameters can't be changed, wherever you have
old(input)
, you could just useinput
. They mean the same thing.