Dafny，forall 分配中的触发器答案

【问题标题】：Dafny, triggers in forall assignmentDafny，forall 分配中的触发器
【发布时间】：2018-11-01 04:49:20
【问题描述】：

在我将序列转换为数组的方法中，我得到了 dafny 的调试器对 VSCode 的建议，但我无法理解它是什么。

    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;
    }

【问题讨论】：

标签： dafny

【解决方案1】：

这不是警告或错误，而只是来自 Dafny 的诊断消息，告诉您它计划如何对 forall 分配进行编码。您可以放心地忽略它。

我同意该消息有点令人困惑，因为它包含字符串“未生成触发器”，而实际上它已经生成了触发器。此消息是由于 Dafny 如何处理 forall 语句的一些内部技术细节。我会提出一个问题来查看它。

【讨论】：