What is an operational abstraction good for?
Program properties (such as specifications and dynamically detected invariants) are useful for a wide variety of software construction, understanding, reuse, and modification tasks. The properties may be examined by a human or used as input to a tool Direct uses of invariants by a human include: • Document code, indicating the structure of its data and computation. • Maintain invariants to avoid introducing bugs; if a property is established at one point in a program, it is likely to be depended on elsewhere, but if the invariant is not documented, it is all to easy to accidentally violate it, introducing a bug in a far-removed part of the program. • Locate unusual conditions that should be brought to a programmer’s attention and may be bugs. • Bootstrap proofs and aid static checkers by providing goals and automating the time-consuming, tedious chore of annotating programs. Uses of invariants by other tools include: • Check assumptions by converting the invariants to assert statements
