Method and apparatus for verifying at runtime an invariant property of a data
structure. In various example embodiments, code that verifies whether a runtime
value of the data structure is consistent with the invariant property is automatically
generated in response to an annotation of the data structure in the source code.
In executing the program, the runtime value of the data structure is compared to
the invariant property in the automatically generated code. If the runtime property
is inconsistent with the invariant property, the program branches to exception
handler code.