Re: [Boost-users] [boost] [review][constrained_value] Review of Constrained Value Library begins today

Subject: Re: [Boost-users] [boost] [review][constrained_value] Review of Constrained Value Library begins today
From: Mika Heiskanen (mika.heiskanen_at_[hidden])
Date: 2008-12-23 12:50:04

David Abrahams wrote:
> I suggest reading through my posts in
> http://groups.google.com/group/comp.lang.c++.moderated/browse_frm/thread/80083ac31a1188da 
> 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.

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. 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 definition does not
seem to imply that the state must already be 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? Does a precondition violation always cause
undefined behaviour, or only if the preconditioned code is
executed? Should I substitute "invariant" for "precondition"
in the above quotes?

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.

--> Mika Heiskanen