Re: [boost] [variant2] Formal review

Subject: Re: [boost] [variant2] Formal review
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2019-04-16 14:58:22

wt., 16 kwi 2019 o 16:47 Steven Watanabe via Boost <boost_at_[hidden]>
napisał(a):

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

Yes, this is what I am encouraging. Treating "effective invariant" as the
same precondition applied to every observer function, as you propose is
impractical, therefore I would rather introduce a new notion. This
shouldn't be that surprising. In the end an ordinary invariant is also the
same precondition and postcondition applied to every function in the
interface: it is a "shorthand notation".

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

It would be very helpful for me if I were demonstrated such example. This
would allow me to revise my claims.

Regards,
&rzej;

>
> > * 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
>
> _______________________________________________
> Unsubscribe & other changes:
> http://lists.boost.org/mailman/listinfo.cgi/boost
>