Daikon generated invariant

Class CommonTree

/*@ invariant this.token.line == this.token.channel; */

/*@ invariant this.token.line == this.token.start; */

/*@ invariant this.token.line == this.token.stop; */

/*@ invariant this.token.charPositionInLine == this.token.index; */

/*@ invariant this.token.charPositionInLine == this.startIndex; */

/*@ invariant this.startIndex == this.stopIndex; */

/*@ invariant this.startIndex == this.childIndex; */

/*@ invariant this.token.type >= 0; */

/*@ invariant this.token.line == 0; */

/*@ invariant this.token.charPositionInLine == -1; */

/*@ invariant this.token.input == null; */

/*@ invariant this.token.text == null; */

/*@ invariant this.startIndex == -1; */

/*@ invariant this.parent == null; */

/*@ invariant this.children == null; */

/*@ invariant this.token.type >= this.token.line; */

/*@ invariant this.token.type > this.token.charPositionInLine; */

/*@ invariant this.token.type > this.startIndex; */

Daikon refined invariant

Below is listed the only property that was maintained after manual inspection.

Class CommonTree

/*@ invariant this.parent == null; */