Dafny - 子串实现
Dafny - Substring implementation
我正在尝试编写一个经过验证的简单子字符串方法实现。
我的方法接受 2 个字符串并检查 str2 是否在 str1 中。
我试图首先弄清楚为什么我的不变量不成立 - Dafny 标记不变量可能在输入时不成立,而我的 pre/post 条件失败。
我对不变量的看法主要有 3 种情况:
1. 循环未能找到索引 i 处的子字符串,还有更多索引需要探索
2. 循环未能找到索引 i 处的子字符串 - 没有更多的索引可供探索
3. 循环在索引 i
找到子串
代码:
method Main() {
var str1,str2 := "Dafny","fn";
var found,offset := FindSubstring(str1,str2);
assert found by
{
calc {
str2 <= str1[2..];
==>
IsSubsequenceAtOffset(str1,str2,2);
==>
IsSubsequence(str1,str2);
==
found;
}
}
assert offset == 2 by
{
assert found && str2 <= str1[2..];
assert offset != 0 by { assert 'D' == str1[0] != str2[0] == 'f'; }
assert offset != 1 by { assert 'a' == str1[1] != str2[0] == 'f'; }
assert offset != 3 by { assert 'n' == str1[3] != str2[0] == 'f'; }
assert !(offset >= 4) by { assert 4 + |str2| > |str1|; }
}
print "The sequence ";
print str2;
print " is a subsequence of ";
print str1;
print " starting at element ";
print offset;
}
predicate IsSubsequence<T>(q1: seq<T>, q2: seq<T>)
{
exists offset: nat :: offset + |q2| <= |q1| && IsSubsequenceAtOffset(q1,q2,offset)
}
predicate IsSubsequenceAtOffset<T>(q1: seq<T>, q2: seq<T>, offset: nat)
{
offset + |q2| <= |q1| && q2 <= q1[offset..]
}
predicate Inv<T>(str1: seq<T>, str2: seq<T>, offset: nat, found: bool)
{
|str1| > 0 && |str2| > 0 && |str1| >= |str2| && offset <= |str1|-|str2| &&
(!found && offset < |str1|-|str2| ==> !(str2 <= str1[offset..])) &&
(!found && offset == |str1| -|str2| ==> !IsSubsequence(str1, str2)) &&
(found ==> IsSubsequenceAtOffset(str1, str2, offset))
}
method FindSubstring(str1: string, str2: string) returns (found: bool, offset: nat)
requires |str2| <= |str1|
ensures found <==> IsSubsequence(str1,str2)
ensures found ==> IsSubsequenceAtOffset(str1,str2,offset)
{
found, offset := str2 <= str1[0..], 0;
assert Inv(str1,str2,offset,found);
while !found && offset <= (|str1| - |str2|)
invariant Inv(str1,str2,offset,found)
{
if str2 <= str1[(offset + 1)..] {
found, offset := true, offset + 1;
} else {
offset := offset + 1;
}
}
Lemma(str1,str2,found,offset);
}
lemma Lemma(str1: string, str2: string, found: bool, offset: nat)
requires !(!found && offset <= (|str1| - |str2|))
requires Inv(str1,str2,offset,found)
ensures found <==> IsSubsequence(str1,str2)
ensures found ==> IsSubsequenceAtOffset(str1,str2,offset)
{}
Link: http://rise4fun.com/Dafny/QaAbU
任何帮助,将不胜感激。
http://rise4fun.com/Dafny/q9BG
1) inv
中的 |str1| > 0 && |str2| > 0
失败,因为此条件未添加到函数 FindSubstring
的要求中
2) 由于 FindSubstring
中的 while 循环体检查 offset+1
的子字符串,while 循环只需要 运行 for offset < (|str1| - |str2|)
因为如果 offset == (|str1| - |str2|)
那么不存在任何满足 str2 <= str1[offset..]
的偏移量
3) 在 inv
中添加量词,确保对于 0 <= k <= offset
处的所有偏移量 k
,不存在任何 k
其中 str2 <= str1[offset..]
调试失败不变量的小建议可能会有所帮助:用 inv
的实际主体替换 inv
调用,dafny 将查明不变量中的失败条件。
希望这是有道理的。
我正在尝试编写一个经过验证的简单子字符串方法实现。 我的方法接受 2 个字符串并检查 str2 是否在 str1 中。 我试图首先弄清楚为什么我的不变量不成立 - Dafny 标记不变量可能在输入时不成立,而我的 pre/post 条件失败。 我对不变量的看法主要有 3 种情况: 1. 循环未能找到索引 i 处的子字符串,还有更多索引需要探索 2. 循环未能找到索引 i 处的子字符串 - 没有更多的索引可供探索 3. 循环在索引 i
找到子串代码:
method Main() {
var str1,str2 := "Dafny","fn";
var found,offset := FindSubstring(str1,str2);
assert found by
{
calc {
str2 <= str1[2..];
==>
IsSubsequenceAtOffset(str1,str2,2);
==>
IsSubsequence(str1,str2);
==
found;
}
}
assert offset == 2 by
{
assert found && str2 <= str1[2..];
assert offset != 0 by { assert 'D' == str1[0] != str2[0] == 'f'; }
assert offset != 1 by { assert 'a' == str1[1] != str2[0] == 'f'; }
assert offset != 3 by { assert 'n' == str1[3] != str2[0] == 'f'; }
assert !(offset >= 4) by { assert 4 + |str2| > |str1|; }
}
print "The sequence ";
print str2;
print " is a subsequence of ";
print str1;
print " starting at element ";
print offset;
}
predicate IsSubsequence<T>(q1: seq<T>, q2: seq<T>)
{
exists offset: nat :: offset + |q2| <= |q1| && IsSubsequenceAtOffset(q1,q2,offset)
}
predicate IsSubsequenceAtOffset<T>(q1: seq<T>, q2: seq<T>, offset: nat)
{
offset + |q2| <= |q1| && q2 <= q1[offset..]
}
predicate Inv<T>(str1: seq<T>, str2: seq<T>, offset: nat, found: bool)
{
|str1| > 0 && |str2| > 0 && |str1| >= |str2| && offset <= |str1|-|str2| &&
(!found && offset < |str1|-|str2| ==> !(str2 <= str1[offset..])) &&
(!found && offset == |str1| -|str2| ==> !IsSubsequence(str1, str2)) &&
(found ==> IsSubsequenceAtOffset(str1, str2, offset))
}
method FindSubstring(str1: string, str2: string) returns (found: bool, offset: nat)
requires |str2| <= |str1|
ensures found <==> IsSubsequence(str1,str2)
ensures found ==> IsSubsequenceAtOffset(str1,str2,offset)
{
found, offset := str2 <= str1[0..], 0;
assert Inv(str1,str2,offset,found);
while !found && offset <= (|str1| - |str2|)
invariant Inv(str1,str2,offset,found)
{
if str2 <= str1[(offset + 1)..] {
found, offset := true, offset + 1;
} else {
offset := offset + 1;
}
}
Lemma(str1,str2,found,offset);
}
lemma Lemma(str1: string, str2: string, found: bool, offset: nat)
requires !(!found && offset <= (|str1| - |str2|))
requires Inv(str1,str2,offset,found)
ensures found <==> IsSubsequence(str1,str2)
ensures found ==> IsSubsequenceAtOffset(str1,str2,offset)
{}
Link: http://rise4fun.com/Dafny/QaAbU 任何帮助,将不胜感激。
http://rise4fun.com/Dafny/q9BG
1) inv
中的 |str1| > 0 && |str2| > 0
失败,因为此条件未添加到函数 FindSubstring
2) 由于 FindSubstring
中的 while 循环体检查 offset+1
的子字符串,while 循环只需要 运行 for offset < (|str1| - |str2|)
因为如果 offset == (|str1| - |str2|)
那么不存在任何满足 str2 <= str1[offset..]
3) 在 inv
中添加量词,确保对于 0 <= k <= offset
处的所有偏移量 k
,不存在任何 k
其中 str2 <= str1[offset..]
调试失败不变量的小建议可能会有所帮助:用 inv
的实际主体替换 inv
调用,dafny 将查明不变量中的失败条件。
希望这是有道理的。