Дафни-функция, недопустимое логическое выражение в цикле while - PullRequest
Новая
       36

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

0 голосов
/ 21 мая 2018

Я новичок в Dafny и получаю некоторые ошибки, которые я не могу понять.

  • в моей программе Dafny для вставки сортировки ( код здесь ), я делаюне понимаю, почему я получаю invalid logical expression в цикле по переменной i.while (i < |input|)
  • в том же коде в части подкачки (input[j := b]; input[j-1 := a];) и я получаю expected method call, found expression.Согласно учебному пособию input[j:=b] заменяет индекс j ввода seq значением b

1 Ответ

0 голосов
/ 21 мая 2018

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

В любом случае, вы можете решить эту проблему, объявив 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.Они означают одно и то же.

...