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]>
> 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,
> > does not guarantee any other special behavior on exception, are never
> > 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
It would be very helpful for me if I were demonstrated such example. This
would allow me to revise my claims.
> > * 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:
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk