Dafny 问题：如何用四种颜色对荷兰国旗问题进行排序？

Question

我正在尝试用 4 种颜色而不是 3 种颜色对荷兰国旗问题进行排序，似乎达夫尼并没有真正验证，我也无法修复它。这是我的代码：

datatype Colour = RED | WHITE | PINK | BLUE
method FlagSort(flag: array<Colour>) returns (w:int, p:int, b:int)
ensures 0 <= w <= p <= b < flag.Length
ensures forall i :: 0 <= i < w ==> flag[i] == RED
ensures forall i :: w <= i < p ==> flag[i] == WHITE
ensures forall i :: p <= i < b ==> flag[i] == PINK
ensures forall i :: b <= i < flag.Length ==> flag[i] == BLUE
ensures multiset(flag[..]) == multiset(old(flag[..]))
modifies flag
{
    var next := 0;
    w, p := 0, 0;
    b := flag.Length;
    while next <= b
    invariant 0 <= w <= p <= next <= b <= flag.Length
    invariant forall i :: 0 <= i < w ==> flag[i] == RED
    invariant forall i :: w <= i < p ==> flag[i] == WHITE
    invariant forall i :: p <= i < next ==> flag[i] == PINK
    invariant forall i :: b <= i < flag.Length ==> flag[i] == BLUE
    invariant multiset(flag[..]) == multiset(old(flag[..]))
    {
        if flag[next] == RED {
            flag[next], flag[w] := flag[w], flag[next];
            w := w + 1;

            if p < w {
                p := p + 1;
            }
            if next < w {
                next := next + 1;
            }
        } else if flag[next] == WHITE {
            flag[next], flag[p] := flag[p], flag[next];
            p := p + 1;
            next := next + 1;
        } else if flag[next] == PINK {
            next := next + 1;
        } else if flag[next] == BLUE {
            b := b - 1;
            flag[next], flag[b] := flag[b], flag[next];
        }
    }
    
}

谁能帮我解决这个问题，谢谢！

Answer 1

我不知道这个问题的解决方案（您可能正在解决一个难题！），但对于 Dafny 在您的代码中发现的三个错误中的每一个，这里都有一些相关建议。

错误 1

当你看到这个：

flag[next], flag[b] := flag[b], flag[next];
                ^^^ index out of range

您可以像这样在之前添加断言：

assert 0 <= b;
assert b < |flags|;
flag[next], flag[b] := flag[b], flag[next];

神奇的是，超出范围的索引将消失，在您的情况下，第一个断言将失败。然后你可以apply verification debugging techniques to move the assertion up.。

错误 2

    while next <= b
    ^^^^^ cannot prove termination, try supplying a decreases clause

问题是它试图插入 decrease 子句b - next，它应该总是递减并以零为界。如果你明确表示，并将鼠标悬停在减少表达式上，它会告诉你“减少表达式总是以零为界”，但你会得到一个新错误：

while next <= b
^^^^^ decreases expression might not decrease
    decreases b - next

您可以做的是在 while 循环的开头添加这一行。

ghost var b_saved,next_saved := b, next;

在 while 循环的末尾，显式添加减少检查：

assert b - next < b_saved-next_saved;

您会看到现在 decreases 子句得到验证，并且您在断言上有错误，您可以在其上应用常规 verification debugging techniques。

错误 3

if flag[next] == RED {
   ^^^^^^^^^^ index out of range.

同样，您可以在此处插入隐式断言：

assert 0 <= next < flag.Length;
if flag[next] == RED {    // No error there

您会在 next < flag.Length 上看到一个下划线。你能做些什么来确保这一点？也许改变一个不变量？