Re: [boost] [variant2] Formal review

Subject: Re: [boost] [variant2] Formal review
From: Steven Watanabe (watanabesj_at_[hidden])
Date: 2019-04-16 14:47:16

AMDG

On 4/16/19 5:18 AM, Andrzej Krzemienski via Boost wrote:
> <snip>However, I propose
> to depart from this model and adapt a more nuanced one. Let's introduce a
> new term: "effective invariant": this is a constraint on object's state
> much as "invariant". It determines what values an object can assume in a
> program where programmers adhere to the important principles that are
> necessary for programs to be correct. We can list some of them:
> 

This is nonsense.  Either something is an invariant
or it isn't.  If it isn't an invariant, then it's
a precondition of every function that assumes that
it is true.  Handling it in this manner isn't wrong,
per se, but it is more complex and therefore more
error prone.  You can't have your cake and eat it, too.
Calling it an "effective invariant," just encourages
treating it as if it were a real invariant.

> * Destructors do not throw exceptions, even if they fail to release
> resources
> 
> * Objects that threw from the operation with basic exception safety, which
> does not guarantee any other special behavior on exception, are never read:
> they are either destroyed or reset,
> 

Never read is too strong.  A more correct statement is
that the object's state should not affect the observable
behavior of the program.  Speculative execution is fine,
for example, as long as the result is eventually thrown
away.  This mainly applies to destructors that do some
kind of actual work, which is relatively rare, but does
happen.

> * Objects that are moved from, unless they explicitly guarantee something
> more, are only destroyed or reset.
> 

This is a very different case from an exception, as you
should usually know statically whether an object has been
moved from and many types do define the state of an object
after a move.

> There may be more of rules like this, which seem quite uncontroversial.
> Note the order: I do not introduce these rules because I want to define
> "effective invariant". these rules are already in place and programmers,
> hopefully, strive to implement them in their programs.
> 

These rules are more or less reasonable, but the
reason that they aren't hard-and-fast is that they're
consequences of the underlying semantics of the
operations in question.

In Christ,
Steven Watanabe