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: David Abrahams (dave_at_[hidden])
Date: 2008-12-23 14:17:41

on Tue Dec 23 2008, Mika Heiskanen <mika.heiskanen-AT-fmi.fi> wrote:

> 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.

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