Я получаю ошибку invalid Ident в строке forall (от is до первой i), кто-нибудь знает почему? Это необычно.
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.
Похоже, что is теперь является ключевым словом в Dafny, поэтому его нельзя использовать в качестве имени переменной.
is на iss и все работает. Кстати, я ответил вам (удалю это), что не могу найти ошибки в: stackoverflow.com/questions/66563130/
- person Theo Deep; 06.04.2021
