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; */