1. A computer-implemented method for verifying at runtime an invariant property of a data structure of a computer program, comprising: automatically generating a first code segment that verifies a runtime value of the data structure is consistent with the invariant property in response to an annotation of the data structure that defines the invariant property of the data structure; comparing the runtime value of the data structure with the invariant property during execution of the program via execution of the first code segment; and performing a programmed action if the runtime value is inconsistent with the invariant property.