Dafny:复制数组区域方法验证
Dafny: copy array region method validation
我正在对几种在考虑验证的情况下创建的语言(Whiley、Dafny 和 Frama-C 等)进行语言比较。我得到了一个函数示例,该函数将一个数组的区域复制到另一个数组目标数组中的不同位置。我想出的规范在 Dafny 中看起来像这样:
method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat, len: nat)
returns (r: array<int>)
// both arrays cannot be null
requires dest != null && src != null
// Source array must contain enough elements to be copied
requires src.Length >= sStart + len
// Destination array must have enough space for copied elements
requires dest.Length >= dStart + len
// Result is same size as dest
ensures r != null
ensures r.Length == dest.Length
// All elements before copied region are same
ensures r[..dStart] == dest[..dStart]
// All elements above copied region are same
ensures r[dStart + len..] == dest[dStart + len..]
// All elements in copied region match src
ensures forall k: nat :: k < len ==> r[dStart + k] == src[sStart + k]
{
if len == 0 { return dest; }
assert len > 0;
var i: nat := 0;
r := new int[dest.Length];
while (i < r.Length)
invariant i <= r.Length
decreases r.Length - i
invariant r.Length == dest.Length
invariant forall k: nat :: k < i ==> r[k] == dest[k]
{
r[i] := dest[i];
i := i + 1;
}
assume r[..] == dest[..];
i := 0;
while (i < len)
invariant i <= len
decreases len - i
invariant r.Length == dest.Length
invariant r.Length >= dStart + i
invariant src.Length >= sStart + i
invariant r[..dStart] == dest[..dStart]
invariant r[(dStart + len)..] == dest[(dStart + len)..]
invariant forall k: nat :: k < i ==> r[dStart + k] == src[sStart + k]
{
r[dStart + i] := src[sStart + i];
i := i + 1;
}
}
在上面的第二个 while 循环中,可能有一些不需要的不变量,因为我已经尽力涵盖了我能想到的所有内容。但是,是的,这并没有证实,我很困惑为什么...
Dafny/copy.dfy(35,4): Error BP5003: A postcondition might not hold on this return path.
Dafny/copy.dfy(17,11): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon19_Else
Dafny/copy.dfy(24,5): anon20_LoopHead
(0,0): anon20_LoopBody
Dafny/copy.dfy(24,5): anon21_Else
(0,0): anon23_Then
Dafny/copy.dfy(35,5): anon24_LoopHead
(0,0): anon24_LoopBody
Dafny/copy.dfy(35,5): anon25_Else
(0,0): anon27_Then
Dafny/copy.dfy(43,16): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
(0,0): anon0
(0,0): anon19_Else
Dafny/copy.dfy(24,5): anon20_LoopHead
(0,0): anon20_LoopBody
Dafny/copy.dfy(24,5): anon21_Else
(0,0): anon23_Then
Dafny/copy.dfy(35,5): anon24_LoopHead
(0,0): anon24_LoopBody
Dafny/copy.dfy(35,5): anon25_Else
Dafny/copy.dfy(35,5): anon27_Else
Dafny program verifier finished with 1 verified, 2 errors
你可以通过添加一个不变量来验证它
invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
如:
while (i < len)
invariant i <= len
decreases len - i
invariant r.Length == dest.Length
invariant r.Length >= dStart + i
invariant src.Length >= sStart + i
invariant r[..dStart] == dest[..dStart]
invariant r[(dStart + len)..] == dest[(dStart + len)..]
invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
invariant forall k: nat :: k < i ==> r[dStart + k] == src[sStart + k]
顺便说一句,我认为如果你愿意,你可以删除许多不变量
method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat, len: nat)
returns (r: array<int>)
// both arrays cannot be null
requires dest != null && src != null
// Source array must contain enough elements to be copied
requires src.Length >= sStart + len
// Destination array must have enough space for copied elements
requires dest.Length >= dStart + len
// Result is same size as dest
ensures r != null
ensures r.Length == dest.Length
// All elements before copied region are same
ensures r[..dStart] == dest[..dStart]
// All elements above copied region are same
ensures r[dStart + len..] == dest[dStart + len..]
// All elements in copied region match src
ensures forall k: nat :: k < len ==> r[dStart + k] == src[sStart + k]
{
if len == 0 { return dest; }
var i: nat := 0;
r := new int[dest.Length];
while (i < r.Length)
invariant i <= r.Length
invariant r[..i] == dest[..i]
{
r[i] := dest[i];
i := i + 1;
}
i := 0;
while (i < len)
invariant i <= len
invariant r[..dStart] == dest[..dStart]
invariant r[(dStart + len)..] == dest[(dStart + len)..]
invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
{
r[dStart + i] := src[sStart + i];
i := i + 1;
}
}
我正在对几种在考虑验证的情况下创建的语言(Whiley、Dafny 和 Frama-C 等)进行语言比较。我得到了一个函数示例,该函数将一个数组的区域复制到另一个数组目标数组中的不同位置。我想出的规范在 Dafny 中看起来像这样:
method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat, len: nat)
returns (r: array<int>)
// both arrays cannot be null
requires dest != null && src != null
// Source array must contain enough elements to be copied
requires src.Length >= sStart + len
// Destination array must have enough space for copied elements
requires dest.Length >= dStart + len
// Result is same size as dest
ensures r != null
ensures r.Length == dest.Length
// All elements before copied region are same
ensures r[..dStart] == dest[..dStart]
// All elements above copied region are same
ensures r[dStart + len..] == dest[dStart + len..]
// All elements in copied region match src
ensures forall k: nat :: k < len ==> r[dStart + k] == src[sStart + k]
{
if len == 0 { return dest; }
assert len > 0;
var i: nat := 0;
r := new int[dest.Length];
while (i < r.Length)
invariant i <= r.Length
decreases r.Length - i
invariant r.Length == dest.Length
invariant forall k: nat :: k < i ==> r[k] == dest[k]
{
r[i] := dest[i];
i := i + 1;
}
assume r[..] == dest[..];
i := 0;
while (i < len)
invariant i <= len
decreases len - i
invariant r.Length == dest.Length
invariant r.Length >= dStart + i
invariant src.Length >= sStart + i
invariant r[..dStart] == dest[..dStart]
invariant r[(dStart + len)..] == dest[(dStart + len)..]
invariant forall k: nat :: k < i ==> r[dStart + k] == src[sStart + k]
{
r[dStart + i] := src[sStart + i];
i := i + 1;
}
}
在上面的第二个 while 循环中,可能有一些不需要的不变量,因为我已经尽力涵盖了我能想到的所有内容。但是,是的,这并没有证实,我很困惑为什么...
Dafny/copy.dfy(35,4): Error BP5003: A postcondition might not hold on this return path.
Dafny/copy.dfy(17,11): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon19_Else
Dafny/copy.dfy(24,5): anon20_LoopHead
(0,0): anon20_LoopBody
Dafny/copy.dfy(24,5): anon21_Else
(0,0): anon23_Then
Dafny/copy.dfy(35,5): anon24_LoopHead
(0,0): anon24_LoopBody
Dafny/copy.dfy(35,5): anon25_Else
(0,0): anon27_Then
Dafny/copy.dfy(43,16): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
(0,0): anon0
(0,0): anon19_Else
Dafny/copy.dfy(24,5): anon20_LoopHead
(0,0): anon20_LoopBody
Dafny/copy.dfy(24,5): anon21_Else
(0,0): anon23_Then
Dafny/copy.dfy(35,5): anon24_LoopHead
(0,0): anon24_LoopBody
Dafny/copy.dfy(35,5): anon25_Else
Dafny/copy.dfy(35,5): anon27_Else
Dafny program verifier finished with 1 verified, 2 errors
你可以通过添加一个不变量来验证它
invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
如:
while (i < len)
invariant i <= len
decreases len - i
invariant r.Length == dest.Length
invariant r.Length >= dStart + i
invariant src.Length >= sStart + i
invariant r[..dStart] == dest[..dStart]
invariant r[(dStart + len)..] == dest[(dStart + len)..]
invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
invariant forall k: nat :: k < i ==> r[dStart + k] == src[sStart + k]
顺便说一句,我认为如果你愿意,你可以删除许多不变量
method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat, len: nat)
returns (r: array<int>)
// both arrays cannot be null
requires dest != null && src != null
// Source array must contain enough elements to be copied
requires src.Length >= sStart + len
// Destination array must have enough space for copied elements
requires dest.Length >= dStart + len
// Result is same size as dest
ensures r != null
ensures r.Length == dest.Length
// All elements before copied region are same
ensures r[..dStart] == dest[..dStart]
// All elements above copied region are same
ensures r[dStart + len..] == dest[dStart + len..]
// All elements in copied region match src
ensures forall k: nat :: k < len ==> r[dStart + k] == src[sStart + k]
{
if len == 0 { return dest; }
var i: nat := 0;
r := new int[dest.Length];
while (i < r.Length)
invariant i <= r.Length
invariant r[..i] == dest[..i]
{
r[i] := dest[i];
i := i + 1;
}
i := 0;
while (i < len)
invariant i <= len
invariant r[..dStart] == dest[..dStart]
invariant r[(dStart + len)..] == dest[(dStart + len)..]
invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
{
r[dStart + i] := src[sStart + i];
i := i + 1;
}
}