// example from page 131
// provable

\javaSource "source/base3";

\programVariables {

int i;

}

\problem {

   \<{ Base o = new SubB(); int res = o.nextId(i); }\> res=i+2

}