7 Dec
2008
7 Dec
'08
9:42 p.m.
a passing test guarantees the invariant (but a failing test need not imply that the invariant is not satisfied). The test is what is implemented (just like the current constraint), but the invariant is only documented/guaranteed.
Hear, hear! In this case, the invariant is what you see in the code but it gets coarsened by the test to account for error.