on Tue Dec 23 2008, Mika Heiskanen
David Abrahams wrote:
I suggest reading through my posts in
http://groups.google.com/group/comp.lang.c++.moderated/browse_frm/thread/800...
which give the arguments in detail.
Thank you for the link, I read the thread from start to finish. It was not clear to me at the end that any agreement was actually reached, in particular with respect to terminology.
Wikipedia says:
a) In computer science, a predicate that, if true, will remain true throughout a specific sequence of operations, is called (an) invariant to that sequence.
b) In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.
I don't care to aargue about terminology, but those two definitions are certainly compatible.
So, an invariant is a value which has already satified a predicate, and if it no longer satisfies one, a logic error must have occurred. On the other hand a precondition is something that must be true before being able to execute some section of code. I can se why an invariant failure should abort, but not why a precondition failure should.
Detecting either a broken supposed-invariant or a failed precondition means there's a logic error in the program and state may already be arbitrarily corrupt.
In particular, Wikipedia says:
If a precondition is violated, the effect of the section of code becomes undefined and thus may or may not carry out its intended work.
So, if were never to execute the section of code, the state could remain perfectly well defined.
The state set up by the calling code must in general be assumed to be already broken. Precondition violations don't just come about because the immediate caller isn't obeying the rules. The immediate caller may have done everything correctly.
The definition does not seem to imply that the state must already be undefined.
There's no such thing as undefined state. The behavior of the code is undefined.
Is this the correct terminology? In the link you gave you seem to have the opinion that a precondition failure is generally fatal, but according to the Wikipedia definition it may not be if you never execute the code.
These are separate quotes from your posts in the link you gave:
If preconditions are broken, your program state is broken, by definition. Trying to recover is generally ill-advised.
Go back to the definition of precondition from Wikipedia: the consequence is undefined behavior.
Which is correct?
Both
Does a precondition violation always cause undefined behaviour,
Yes
or only if the preconditioned code is executed?
If the code isn't executed, the precondition doesn't apply. There's a precondition on integer division that the divisor be nonzero. If you call a variable "divisor" and never actually use it as a divisor, there's no precondition violation. If you set preconditions on your function, they apply to your callers, and thus are true or not at its interface, not to some point during the execution after you've done some checking.
Should I substitute "invariant" for "precondition" in the above quotes?
No
Sorry if I am being a nuisance. I thought I had already understood the terminology, but reading the thread you mentioned made it a fuzzy again.
Hope this helped. -- Dave Abrahams BoostPro Computing http://www.boostpro.com