微信公众号搜"智元新知"关注
微信扫一扫可直接关注哦!

Dafny for循环与forall语句一起使用?

如何解决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 举报,一经查实,本站将立刻删除。