Dafny 无效的身份

Question

我在 forall 行（从 is 到第一个 i）中收到 invalid Ident 错误，有人知道为什么吗？这很不寻常。

predicate SumMaxToRight(v:array<int>,i:int,s:int)
   reads v
   requires 0<=i<v.Length
  {forall l, is {:induction l} :: 0<=l<=i && is==i+1 ==> Sum(v,l,is)<=s}

版本 3.0.0.

Answer 1

看来is现在是Dafny中的关键字，所以不能用作变量名。