analysis

Object invariant

class LinkedList { Link header; … }

class Link { int element; Link next; … }

Object invariant:

header ¹ null

header.element = 0

size(header.closure(next)) ³ 1


	This is an actual invariant that Daikon detected.
	Object invariants are checked at multiple program points.