JML typing error: a memory state is needed here (\at missing?)

Question

I've been trying to fix an error in my JML program, but I haven't been able to do it. It's a typing error that references to a file, "Practi.jc" that I have no clue about where it is neither.

//@+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);
    }
}

I expected to check the correction of the function additionV through the program Krakatoa in Ubuntu, but the following error is shown through the screen: File "Practi.jc", line 68, characters 49-65: typing error: a memory state is needed here (\at missing?)