如何解决Dafny for循环与forall语句一起使用?
我已经在Dafny中工作了一段时间,如果不得不使用for循环,我使用了while
语句,因为我认为for循环在Dafny中是不存在的。
但是,在此链接(Dafny,triggers in forall assignment)上,我看到代码使用forall
语句作为for
method toArrayConvert(s:seq<int>) returns(res:array<int>)
requires |s|>0;
ensures |s| == res.Length;
ensures forall i::0<=i<res.Length ==> s[i] == res[i];
{
res :=new int[|s|];
forall i|0<=i && i<|s| {res[i]:=s[i];} /*on this line I get the following*/
// rewrite: forall i#inv: int {:trigger res[i#inv]} | 0 <= i#inv && i#inv < |s| { res[i#inv] := s[i#inv]; }
//Not generating triggers for "res[i#inv] == s[i#inv]".
return res;
}
我认为forall
仅在验证点(断言,后置条件,不变式...)中用作量词,对于循环无效。我理解错了吗?
PS:
forall i|0<=i && i<|s| {res[i]:=s[i];}
作者
forall i: int {:trigger res[i]} | 0 <= i && i < |s| { res[i] := s[i]; }
就像可以看到的代码一样:
method toArrayConvert(s:seq<int>) returns(res:array<int>)
requires |s|>0;
ensures |s| == res.Length;
ensures forall i::0<=i<res.Length ==> s[i] == res[i];
{
res :=new int[|s|];
//forall i|0<=i && i<|s| {res[i]:=s[i];} /*on this line I get the following*/
forall i: int {:trigger res[i]} | 0 <= i && i < |s| { res[i] := s[i]; }
//Not generating triggers for "res[i#inv] == s[i#inv]".
return res;
}
它给了我错误:unresolved identifier: i
这是怎么回事?是否有必要像调试器所说的那样使用i#inv
之类的东西而不是i
?但这也会给我带来错误。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。