analysis

Pointer experiment

•Data structures from Weiss’s Data Structures and Algorithm Analysis in Java

•Identified goal invariants by reading book

•Added linearization and data splitting to Daikon

•Results

–90-100% of goal invariants

–few extraneous invariants


	First five data structures from the text.

	Found places where the “expected” invariant doesn’t hold. For instance, one data structure constructor initialized an index to an out-of-bounds value that it never took on again, because the first operation was sure to increment it before using it.

	Output includes both functional invariants and usage properties.

	I didn’t tune the engine to this set of invariants -- just the invariants that were already in the engine.
	I did have to enhance the redundant invariant elimination rules (the logical implication tests) to avoid introducing many irrelevant invariants.