|
|
|
[This is a laundry
list of potential uses for invariants.
I'm trying to motivate why one would care about invariants.]
|
|
Better programs when
invariants are used in their design.
But here I will focus on uses of invariants in already-constructed
programs.
|
|
Documentation is
guaranteed to be up-to-date; for assert, is machine-checkable.
|
|
Invariants
established at one point may be depended upon elsewhere. This was the original motivation for the
system. There’s evidence that
maintenance introduces many bugs (and anecdotal evidence that some are due to
violating invariants).
|
|
The next four are
arguably more useful with dynamic than with static invariants:
|
|
Unusual
(exceptional) conditions may indicate bugs or special cases that should be
brought to a programmer’s attention.
(But finding bugs isn’t my focus or what I consider the tool’s
strength, though it was effective at that task. I would rather prevent a bug than have to
find it any day.)
|
|
Value coverage may
be inadequate even if a test suite covers every line of a program. [Example:
only small values.]
|
|
Use invariants like
profile-directed compilation, but at a higher and possibly more valuable
level (cf “Value Profiling and Optimization” by Calder et al).
|
|
Bootstrap
proofs: or, formally prove the
invariants. In theorem-proving, many
consider it harder to determine what to prove than to actually do the proof. [Don’t say “’turn the crank”; it belittles
theorem-proving.] [If you prove the
property, the system becomes sound:
but probably don’t raise this red flag yet.]
|
|
|
|
Now, I’ll try to
convince you that this is at least possible.
|
