我有一个数组CCD_ 1,其中包含一个长度为CCD_,CCD_ 3是其中包含长度为CCD_。注:p
和l
不是阵列的长度
目的是查看pat
中包含的字符串是否存在于line
中。如果是,此方法应返回单词第一个字母的line
中的索引,否则应返回line
0。
给我们"找不到可触发的项"错误的不变量是ensures exists j :: ( 0<= j < l) && j == pos;
和invariant forall j :: 0 <= j < iline ==> j != pos;
我对循环的逻辑是,当它们在循环中时,没有找到索引。确保是在遇到索引时。
可能出了什么问题?
这是代码:
method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int)
requires line!=null && pat!=null;
requires 0 <= l < line.Length;
requires 0 <= p < pat.Length;
ensures exists j :: ( 0<= j < l) && j == pos;
{
var iline:int := 0;
var ipat:int := 0;
var initialPos:int := -1;
while(iline<l && ipat<pat.Length)
invariant 0<=iline<=l;
invariant 0<=ipat<=pat.Length;
invariant forall j :: 0 <= j < iline ==> j != pos;
{
if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){
if(initialPos==-1){
initialPos := iline;
}
ipat:= ipat + 1;
}
else{
if(ipat>0){
if(line[iline] == pat[ipat-1]){
initialPos := initialPos + 1;
}
}
ipat:=0;
initialPos := -1;
}
if(ipat==p){
return initialPos;
}
iline := iline + 1;
}
return initialPos;
}
我收到以下错误:Dafny输出的屏幕截图
这是rise4fun的代码。
我认为你不需要使用量词来做出那些有问题的断言:
exists j :: ( 0<= j < l) && j == pos;
可以更好地写成:
0 <= pos < l
和
forall j :: 0 <= j < iline ==> j != pos
含义与相同
pos >= iline
通过移除量化器,您就不需要求解器实例化量化器,因此不需要触发器。
此外,我认为如果找不到模式,您的方法将返回-1
。所以你需要考虑到这一点来进行验证:
method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int)
requires line!=null && pat!=null
requires 0 <= l < line.Length
requires 0 <= p < pat.Length
ensures 0 <= pos < l || pos == -1
{
var iline:int := 0;
var ipat:int := 0;
pos := -1;
while(iline<l && ipat<pat.Length)
invariant 0<=iline<=l
invariant 0<=ipat<=pat.Length
invariant -1 <= pos < iline
{
if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){
if(pos==-1){
pos := iline;
}
ipat:= ipat + 1;
} else {
if(ipat>0){
if(line[iline] == pat[ipat-1]){
pos := pos + 1;
}
}
ipat:=0;
pos := -1;
}
if(ipat==p) {
return;
}
iline := iline + 1;
}
return;
}
http://rise4fun.com/Dafny/J4b0