Richer types of invariant
Object/class invariants
node.left.value < node.right.value
string.data[string.length] = ’\0’
Pointers (recursive data structures)
tree is sorted
Conditionals
if  proc.priority < 0 then
    proc.status = active
ptr = null  or  *ptr > i
In this talk I will discuss three other types of invariant.

[Make it clear that this is past work.  Not “I will need to” but “I had to” or “I did”.]

Object/class invariants are well-formedness conditions for data structures.  They require examining multiple program points, not just one.  They are true at entry to and exit from each public method.

Pointers are a challenge only in the context of recursive data structures, where the instrumentation may have to traverse arbitrarily many links.  Otherwise we can just view a pointer as a record with two fields:  the address and the content.

Disjunctions are a variety of conditional, because implications and disjunctions are interconvertible

Goal is to incorporate this within the current infrastructure (with minimal change), subject to constraints on resources (primarily my time).