(Dafny) 数组排序 - 循环不变量
(Dafny) Sorting an array - loop invariant
这是一个简单的排序算法写在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) 可能不会被循环维护。
这是为什么？
如何猜测首先需要不变量 forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n] ？
我试图在纸上证明这个程序，但在构造内循环的不变量时我不需要这个不变量。
为什么 sorted(a,j,i+1) 没有额外的不变量就无法维护？
记住验证循环不变量需要什么。它需要从满足循环不变式的任意状态开始，执行循环体，然后证明你在满足循环不变式的状态结束。换句话说，不能假定循环不变量之外的任何东西。
没有额外的循环不变量，没有什么能阻止区域 a[0..j] 包含大于 a[j..i+1] 的元素。特别是，在执行循环时，我们知道 a[j-1] > a[j]，所以说 a[j-1] 不也大于每个 a[k] 和 k >= j？
我们如何猜测额外不变量？
考虑插入排序的内部循环的一种方法是它保持一种不变的类型，例如“a 除了在 a[j] 之外被排序”。事实上，它维护了一些稍微更强的东西，即“a 是排序的，除了 a[j] 可能比 [=23= 的任何 a[k] 乱序（即更小） ].
我们可以将其表示为您的 sorted 谓词的修改版本：
invariant forall m,n | 0 <= m < n < i+1 && n != j :: a[m] <= a[n]
表示 a 在所有索引对 中排序，除了 第二个索引是 j.
事实上，内部循环仅使用此不变量进行验证（即，没有 sorted 不变量或 "extra" 不变量）。
我们可以将您的 "extra" 不变量视为与 sorted(a,0,j) 和 sorted(a,j,i+1) 结合时表达此更简洁不变量的另一种方式。对于任何一对指数，如果它们都低于 j，则适用 sorted(a,0,j)。如果它们都落在 j 以上或处于 j，则适用 sorted(a,j,i+1)。如果一个低于 j 并且一个严格高于 j，则适用额外不变量。唯一剩下的情况是当较大的索引恰好是 j 时，但这种情况已被简洁的语句排除。
这是一个简单的排序算法写在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) 可能不会被循环维护。
这是为什么？
如何猜测首先需要不变量
forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n]？我试图在纸上证明这个程序，但在构造内循环的不变量时我不需要这个不变量。
为什么 sorted(a,j,i+1) 没有额外的不变量就无法维护？
记住验证循环不变量需要什么。它需要从满足循环不变式的任意状态开始，执行循环体，然后证明你在满足循环不变式的状态结束。换句话说，不能假定循环不变量之外的任何东西。
没有额外的循环不变量，没有什么能阻止区域 a[0..j] 包含大于 a[j..i+1] 的元素。特别是，在执行循环时，我们知道 a[j-1] > a[j]，所以说 a[j-1] 不也大于每个 a[k] 和 k >= j？
我们如何猜测额外不变量？
考虑插入排序的内部循环的一种方法是它保持一种不变的类型，例如“a 除了在 a[j] 之外被排序”。事实上，它维护了一些稍微更强的东西，即“a 是排序的，除了 a[j] 可能比 [=23= 的任何 a[k] 乱序（即更小） ].
我们可以将其表示为您的 sorted 谓词的修改版本：
invariant forall m,n | 0 <= m < n < i+1 && n != j :: a[m] <= a[n]
表示 a 在所有索引对 中排序，除了 第二个索引是 j.
事实上，内部循环仅使用此不变量进行验证（即，没有 sorted 不变量或 "extra" 不变量）。
我们可以将您的 "extra" 不变量视为与 sorted(a,0,j) 和 sorted(a,j,i+1) 结合时表达此更简洁不变量的另一种方式。对于任何一对指数，如果它们都低于 j，则适用 sorted(a,0,j)。如果它们都落在 j 以上或处于 j，则适用 sorted(a,j,i+1)。如果一个低于 j 并且一个严格高于 j，则适用额外不变量。唯一剩下的情况是当较大的索引恰好是 j 时，但这种情况已被简洁的语句排除。