Dafny 函数，while 循环中的逻辑表达式无效

Question

我是 Dafny 的新手，遇到了一些我无法弄清楚的错误。

在我的插入排序 Dafny 程序中 (the code is here)，我不明白为什么我在变量 i 的 While 循环中得到 invalid logical expression。 while (i < |input|)
在交换部分 (input[j := b]; input[j-1 := a];) 的相同代码中，我也得到 expected method call, found expression。根据教程 input[j:=b] 正在用 b

Answer 1

第一个错误是因为您被声明为 function 而不是 method。在 Dafny 中，function 的主体应该是一个表达式，而不是一系列语句。因此，当解析器看到关键字 "while" 时，它意识到出了点问题（因为 "while" 不能成为语句的一部分）并给出一条错误消息。我不确定为什么错误消息指的是 "logical" 表达式。

无论如何，您可以通过声明 method 而不是 function 来解决这个问题。

您需要一种方法，因为您使用的是命令式算法而不是函数式算法。的确，您需要一个子例程来计算其输出作为其输入的函数而没有副作用。但是，在 Dafny 中，当您想要执行此操作的方式涉及命令式构造（如赋值和 while 循环）时，您仍然会为此使用 method。

第二个问题是 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。他们的意思是一样的。

Dafny 函数，while 循环中的逻辑表达式无效

Dafny function, invalid logical expression on while loop

verification

insertion-sort

z3

dafny