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

编程问答 2022-06-07

问题描述

我已经在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 (将#修改为@）

dafnydebuggingdebuggingdebuggingfor-looptriggerswhile-loop