Structure: extern f(i : Int) : Int = "{i} + 1" state x : Int query foo() f(x) op setX(y : Int) x = y;public Integer foo() { return _var62;}assert(result == this._var62);public void setX(Integer y) { _var62 = ((y) + 1);}assert(y == this._var62 - 1);