时间戳

首页 > 解决方案 > Dafny，forall 分配中的触发器

dafny - Dafny，forall 分配中的触发器

问题描述

在我将序列转换为数组的方法中，我得到了 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

解决方案

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

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

推荐阅读