Ошибка ввода JML: здесь необходимо состояние памяти (\at отсутствует?)

Question

Я пытался исправить ошибку в своей программе JML, но мне это не удалось. Это опечатка, которая ссылается на файл «Practi.jc», о том, где он находится, я понятия не имею.

      //@+CheckArithOverflow=no

/*@ axiomatic Addition{
@logic integer sum(int [] x, integer n);
@axiom sum_vector_empty:
@\forall int x[];sum(x,0)==0;
@axiom sum_vector:
@\forall int  x[], integer n; n>=0 ==> sum(x,n+1)==sum(x,n)+x[n];
@ }
@*/

public class main
{
/*@ requires (0 < v.length) && (v!=null);
    @ ensures (\result==sum(v,v.length));
     @*/
    public static int additionV (int v[])
    {
        int i = 0;
        int res = 0;
      /*@ loop_invariant (0<=i < v.length) && (res == sum(v,i)) &&
@(\forall integer j; (0 <= j < i) ==> (v[j] == \at (v[j], Pre)));
         @ loop_variant (v.length-i);
         @*/
        while (i < v.length)
        {
            res = res + v[i];
            i = i + 1;
        }
        return (res);
    }
}

Я рассчитывал проверить исправление функции addV через программу Krakatoa в Ubuntu, но на экране высвечивается следующая ошибка: Файл "Practi.jc", строка 68, символы 49-65: ошибка ввода: необходимо состояние памяти здесь (\отсутствует?)