Linearize data structures
•
Traverse pointer-directed data
structures
•
Present to invariant engine as
sequence
–
cyclicity determined by front end
[Don’t say “serialize”, which means something in Java; say “linearize”.]
[Don’t say “optimized”, say “designed”.]
No change to engine required
Need not be frequent:
•
stop traversing the data structure when not of interest
•
incrementally maintain
•
backoff (less frequent checking once it has been satisfied many times)
•
integrate with garbage collection
Such invariants require traversal; the same is true for arrays, but there the size is known or at least is generally not enormous.
