Dafny,Dutch Flag,循环不变量可能不会被循环维护
Dafny, Dutch Flag, loop invariant might not be maintained by the loop
在下面的程序中,我正在创建类似荷兰国旗问题的问题,并遵循同样提供的逻辑 here
该程序对 0s、1s 和 2s 的数组进行排序,所有 1s 在开头,0s 在中间,2s 在末尾。 [1,1,1,0,0,2,2,2]
。
但是在循环不变量中,我得到错误 This loop invariant might not be maintained by the loop.
最初,i
和 j
在索引 0 处,k
在最后一个索引处。逻辑是如果 j 看到 2 就向上移动,与 k 交换,如果看到 0 只是 j
向上移动,k 减少,如果看到 1 与 i
交换并且 i
和 j
增加。
代码也在rise4fun
method sort(input: array?<int>)
modifies input
requires input !=null;
requires input.Length>0;
requires forall x::0<=x<input.Length ==> input[x]==0||input[x]==1||input[x]==2;
ensures sorted(input);
{
var k: int := input.Length;
var i, j: int := 0 , 0;
while(j != k )
invariant 0<=i<=j<=k<=input.Length;
/* the following invariants might not be maintained by the loop.*/
invariant forall x:: 0<=x<i ==> input[x]==1;
invariant forall x:: i<=x<j ==> input[x]==0;
invariant forall x:: k<=x<input.Length ==> input[x]==2;
invariant forall x:: j<=x<k ==> input[x]==0||input[x]==1||input[x]==2;
decreases if j <= k then k - j else j - k
{
if(input[j] == 2){
swap(input, j, k-1);
k := k - 1;
} else if(input[j] == 0){
j := j + 1;
} else {
swap(input, i, j);
i:= i + 1;
j := j + 1;
}
}
}
这里是 swap
方法和 sorted
谓词
predicate sorted(input:array?<int>)
requires input!=null;
requires input.Length>0;
reads input;
{
forall i,j::0<=i<j<input.Length ==> input[i]==1 || input[i]==input[j] || input[j]==2
}
method swap(input: array?<int>, n:int, m:int)
modifies input;
requires input!=null;
requires input.Length>0;
requires 0<=n<input.Length && 0<=m<input.Length
{
var tmp : int := input[n];
input[n] := input[m];
input[m] := tmp;
}
问题是 swap
没有后置条件。默认的后置条件是 true
,所以 swap
的规范说明它以任意方式改变数组。
当验证器在方法 sort
的主体中看到对 swap
的调用时,它只关注 swap
的规范 --- 而不是它的主体。因此,在调用 swap
之后,数组中可能包含任何值,至少就验证者而言是这样。因此,无法证明与数组内容有关的任何不变量也就不足为奇了。
swap
的以下规范应该有效:
method swap(input: array?<int>, n:int, m:int)
modifies input;
requires input!=null;
requires input.Length>0;
requires 0<=n<input.Length && 0<=m<input.Length
ensures n < m ==> input[..] == old( input[0..n] + [input[m]] + input[n+1..m] + [input[n]] + input[m+1..] ) ;
ensures n==m ==> input[..] == old(input[..])
ensures n > m ==> input[..] == old( input[0..m] + [input[n]] + input[m+1..n] + [input[m]] + input[n+1..] ) ;
这也应该
method swap(input: array?<int>, n:int, m:int)
modifies input;
requires input!=null;
requires input.Length>0;
requires 0<=n<input.Length && 0<=m<input.Length
ensures input[n] == old( input[m] ) ;
ensures input[m] == old( input[n] ) ;
ensures forall i | 0 <= i < input.Length && i != n && i != m :: input[i] == old(input[i])
在下面的程序中,我正在创建类似荷兰国旗问题的问题,并遵循同样提供的逻辑 here
该程序对 0s、1s 和 2s 的数组进行排序,所有 1s 在开头,0s 在中间,2s 在末尾。 [1,1,1,0,0,2,2,2]
。
但是在循环不变量中,我得到错误 This loop invariant might not be maintained by the loop.
最初,i
和 j
在索引 0 处,k
在最后一个索引处。逻辑是如果 j 看到 2 就向上移动,与 k 交换,如果看到 0 只是 j
向上移动,k 减少,如果看到 1 与 i
交换并且 i
和 j
增加。
代码也在rise4fun
method sort(input: array?<int>)
modifies input
requires input !=null;
requires input.Length>0;
requires forall x::0<=x<input.Length ==> input[x]==0||input[x]==1||input[x]==2;
ensures sorted(input);
{
var k: int := input.Length;
var i, j: int := 0 , 0;
while(j != k )
invariant 0<=i<=j<=k<=input.Length;
/* the following invariants might not be maintained by the loop.*/
invariant forall x:: 0<=x<i ==> input[x]==1;
invariant forall x:: i<=x<j ==> input[x]==0;
invariant forall x:: k<=x<input.Length ==> input[x]==2;
invariant forall x:: j<=x<k ==> input[x]==0||input[x]==1||input[x]==2;
decreases if j <= k then k - j else j - k
{
if(input[j] == 2){
swap(input, j, k-1);
k := k - 1;
} else if(input[j] == 0){
j := j + 1;
} else {
swap(input, i, j);
i:= i + 1;
j := j + 1;
}
}
}
这里是 swap
方法和 sorted
谓词
predicate sorted(input:array?<int>)
requires input!=null;
requires input.Length>0;
reads input;
{
forall i,j::0<=i<j<input.Length ==> input[i]==1 || input[i]==input[j] || input[j]==2
}
method swap(input: array?<int>, n:int, m:int)
modifies input;
requires input!=null;
requires input.Length>0;
requires 0<=n<input.Length && 0<=m<input.Length
{
var tmp : int := input[n];
input[n] := input[m];
input[m] := tmp;
}
问题是 swap
没有后置条件。默认的后置条件是 true
,所以 swap
的规范说明它以任意方式改变数组。
当验证器在方法 sort
的主体中看到对 swap
的调用时,它只关注 swap
的规范 --- 而不是它的主体。因此,在调用 swap
之后,数组中可能包含任何值,至少就验证者而言是这样。因此,无法证明与数组内容有关的任何不变量也就不足为奇了。
swap
的以下规范应该有效:
method swap(input: array?<int>, n:int, m:int)
modifies input;
requires input!=null;
requires input.Length>0;
requires 0<=n<input.Length && 0<=m<input.Length
ensures n < m ==> input[..] == old( input[0..n] + [input[m]] + input[n+1..m] + [input[n]] + input[m+1..] ) ;
ensures n==m ==> input[..] == old(input[..])
ensures n > m ==> input[..] == old( input[0..m] + [input[n]] + input[m+1..n] + [input[m]] + input[n+1..] ) ;
这也应该
method swap(input: array?<int>, n:int, m:int)
modifies input;
requires input!=null;
requires input.Length>0;
requires 0<=n<input.Length && 0<=m<input.Length
ensures input[n] == old( input[m] ) ;
ensures input[m] == old( input[n] ) ;
ensures forall i | 0 <= i < input.Length && i != n && i != m :: input[i] == old(input[i])