Функция Dafny, недопустимое логическое выражение в цикле while

Первая ошибка заключается в том, что вы объявлены function, а не method. В Dafny тело function должно быть выражением, а не последовательностью операторов. Итак, когда синтаксический анализатор видит ключевое слово «пока», он понимает, что что-то не так (поскольку «пока» не может быть частью оператора) и выдает сообщение об ошибке. Я не уверен, почему сообщение об ошибке относится к «логическому» выражению.

В любом случае, вы можете решить эту проблему, объявив method, а не function.

Вам нужен метод, потому что вы используете императивный алгоритм, а не функциональный алгоритм. Это правда, что вам нужна подпрограмма, которая вычисляет свои выходные данные как функцию своих входных данных без побочных эффектов. Но в Dafny вы по-прежнему используете для этого method, когда вы хотите сделать это с помощью императивных конструкций, таких как присваивания и циклы while.

Вторая проблема заключается в том, что input[j := b] является выражением, тогда как синтаксический анализатор ожидал оператора. Вы можете исправить это, переписав input[j := b]; input[j-1 := a]; как input := input[j:=b]; input := input[j-1];.

К сожалению, это приведет к другой проблеме, которая заключается в том, что в Dafny входные параметры не могут быть назначены. Так что вам лучше сделать другую переменную. Смотрите ниже, как я это сделал.

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;
        ...
    }
}

Кстати, поскольку входные параметры изменить нельзя, везде, где у вас есть old(input), вы можете просто использовать input. Они означают одно и то же.