2

这是一个用Dafny编写的简单排序算法：

predicate perm(a:array<int>, b:array<int>)
    requires a != null && b != null
    reads a,b
{
    multiset(a[..]) == multiset(b[..])
}

predicate sorted(a:array<int>, min:int, max:int)
    requires a != null
    requires 0 <= min <= max <= a.Length 
    reads a
{
    forall i,j | min <= i < j < max :: a[i] <= a[j] 
}
method sort(a:array<int>)
    requires a != null
    requires a.Length >= 1
    modifies a
    ensures perm(a,old(a))
    ensures sorted(a, 0, a.Length)
    
{
    var i := 1;
    while i < a.Length 
        invariant perm(a,old(a))
        invariant 1 <= i <= a.Length
        invariant sorted(a, 0, i)       
        decreases a.Length-i
    {
        var j := i;
    
        while j > 0 && a[j-1] > a[j] 
            invariant perm(a,old(a))
            invariant 1 <= i <= a.Length-1
            invariant 0 <= j <= i
            invariant sorted(a,0,j)
            invariant sorted(a,j,i+1) //MIGHT NOT BE MAINTAINED IF I REMOVE THE NEXT INVARIANT
            invariant forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n]
            decreases j
        {
            a[j], a[j-1] := a[j-1], a[j];
            j := j-1;
        }
        i := i+1;
    }
}

代码没有错误。但是，如果我从forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n]内部循环中删除不变量，Dafny 会告诉我循环sorted(a,j,i+1)可能不会维护不变量。

  1. 这是为什么？

  2. 怎么能猜到一 forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n] 开始就需要不变量呢？

    我试图在纸上证明这个程序，但是在构造内部循环的不变量时我不需要这个不变量。

4

1 回答 1

1

为什么sorted(a,j,i+1)不保持没有额外的不变量？

记住验证循环不变量需要什么。它需要从满足循环不变量的任意状态开始，执行循环体，然后证明您以满足循环不变量的状态结束。换句话说，除了循环不变量之外，什么都不能假设。

如果没有额外的循环不变量，没有什么能阻止该区域a[0..j]包含大于 的元素a[j..i+1]。特别是，当循环正在执行时，我们知道a[j-1] > a[j]，所以说它a[j-1]也不比every a[k]with大k >= j吗？

我们如何猜测额外的不变量？

考虑插入排序的内部循环的一种方法是，它保持一种不变的类型，例如“a除了在a[j]”之外已排序。事实上，它维护了一些稍强的东西，即 "a已排序，但它a[j]可能比任何a[k]带有k < j.

我们可以将其表示为您的sorted谓词的修改版本：

invariant forall m,n | 0 <= m < n < i+1 && n != j :: a[m] <= a[n]

这表示除了a第二个索引为.j

事实上，内部循环仅使用这个不变量进行验证（即，没有任何一个sorted不变量或“额外”不变量）。

我们可以将您的“额外”不变量视为与sorted(a,0,j)and结合时表达这个更简洁的不变量的另一种方式sorted(a,j,i+1)。对于任何一对索引，如果它们都低于j，则sorted(a,0,j)适用。如果它们都高于或位于j，则sorted(a,j,i+1)适用。如果一个低于j并且一个严格高于j，则应用额外的不变量。唯一剩下的情况是较大的索引恰好是j，但简明陈述排除了这种情况。

于 2017-07-30T05:42:19.563 回答