- status changed from new to accepted
- milestone set to 1.0.0
(9)
Class invariants: I have an observation, not about yuor library but the way
invariants are handled in DbC methodology. As a "contract" (involving two
parties) they make sense when checked after any (public) function call:
they are a sort of postcondition that is the same for every function: class
implementer "ensures" and class user "expects". But when checked before any
function execution they are more like a C-assert: the function "expects",
but who is supposed to "ensure"? Only any other public function of that
class -- but this is already verified by checking postconditions. Somehow
checking invariants before function execution is checking the same thing
twice.
:) I'm glad you raise this issue, I take it that the docs allowed you to gain a good understand of Contract Programming. Here what N1613 says to your point:
http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2004/n1613.pdf
``
7.2 Can we call the invariant less often?
It could also be argued that the invariant should only be checked as a function
exits. The invariant in the precondition would automatically hold because
of an earlier postcondition. The programmer could be malicious and
by-pass the mechanism by using public data, friends, function pointers and
templated member functions, but why protect against that? Thus we could
reduce the calls to the invariant to a half which improves debug performance.
(Remark: checking the invariant more often would detect memory
corruption errors earlier, but it is debatable whether this is any better since
the error would probably not be due to an error in the class where the invariant
failed.)
``
So yes, you are correct.
If you find my reasoning even a bit convincing, perhaps it is worth
considering adding another config macro:
CONTRACT_CONFIG_NO_CLASS_INVARIANTS_ON_FUNCTION_ENTRY, that would disable
invariant checking before function or destructor call, but still check them
after function or constructor call?
Provide such a configuration macro.
Log in to post a comment.