[boost] Re: Re: STL containers with contracts, any interest?

From: Yariv Tal (yariv_tal2003_at_[hidden])
Date: 2005-02-23 11:44:59

"christopher diggins" <cdiggins_at_[hidden]> wrote in message
news:004b01c519c0$f3b185c0$d9958242_at_heronnest...
> ----- Original Message ----- 
> From: "Yariv Tal" <yariv_tal2003_at_[hidden]>
> To: <boost_at_[hidden]>
> Sent: Wednesday, February 23, 2005 9:05 AM
> Subject: [boost] Re: STL containers with contracts, any interest?
>
>
> > You may want to take a look at a small DbC library I'm working on called
> > ensure++.
> >
> > You can find it on sourceforge, at
http://sourceforge.net/projects/ensure/
> >
> > It allows you to write the post() part conditions at the _beginning_ of
> > your
> > method, near the pre conditions.
> > Quick example: (note that I already have a plan on how to remove the
need
> > for the CONDITIONS, BODY & ENDBODY macros. Software is a constant
process
> > of
> > improvement :)   )
> >
> > void push_back(const T& x)  {
> >      CONDITIONS
> >            ENSURE(!post(&vector_contract::empty, this));
> >            ENSURE(post(&vector_contract::size, this) == size() + 1);
> >             // let's ensure (some of) the strong exception guarenttee -
> >             //no change in size in case of exception
> >            EXCEPTIONAL(post(&vector_contract::size, this) == size());
> >      BODY
> >            inherited::push_back(x);
> >      ENDBODY
> > }
> >
> > void pop_back() {
> >
> >      CONDITIONS
> >            REQUIRE(!empty());
> >            ENSURE(post(&vector_contract::size, this) == size() - 1);
> >             // let's ensure (some of) the strong exception guarenttee -
> >             //no change in size in case of exception
> >            EXCEPTIONAL(post(&vector_contract::size, this) == size());
> >      BODY
> >            inherited::pop_back();
> >      ENDBODY
> > }
> >
> > [I'm writing this example on the fly - so don't kill me if it doesn't
> > quite
> > compile after you download the lib]
>
> Hi Yariv,
>
> This appears to be very cool code. However, I am at a loss to find a good
> reason I would want to place post-conditions at the beginning of a code
> block given that the contract classes are always one-liners (e.g.
> inherited::fxn() ). Any comments?
>
True. For one liners you are probably right.
However, if you want to allow conditionally removing the contract code
(i.e. for release code) you are still left with the definitions and code of
taking
the "old_value" in some of your checks, i.e.:
    void push_back(const T& x)  {
      size_t old_size = size(); // in release version this is unwanted
code...
      inherited::push_back(x);
      POST(!empty());
      POST(size() == old_size + 1);
    }

The solution I propose never actually defines named temp variables, so
all of the contracts code can be removed in release code (of course,
your approach is to change the vector typedef so you also have no problem,
but in general this could be a problem).
Theoretically an optimizer should be able to remove the code that stores
the old value - if you it can see the code of the methods called for getting
that value in the first place (to ensure there are no side effects) and
assuming it is allowed to remove named temporary variables (I think
the standard says it isn't...)

> The EXCEPTIONAL(...) macro is a very good idea which I overlooked, and
will
> be borrowing ;-)
>
enjoy.
I would love it if you add a comment referencing the ensure++ lib for this,
but it's up to you (in other words: I don't claim to have any special rights
on the idea).

> Concerning:
> > ENSURE(post(&vector_contract::size, this) == size() - 1);
>
> If I understand this correctly, the "vector_contract::" is superflous is
it
> not?
>
I'm not sure. Maybe this is something I am carrying from MSVC6, maybe
vc7.1 requires it, maybe the standard requires it or maybe it was never
needed.
Anyone out there knows the answer?

> Thanks for sharing this with us!
>
> Christopher Diggins
> Object Oriented Template Library (OOTL)
> http://www.ootl.org
>
> _______________________________________________
> Unsubscribe & other changes:
http://lists.boost.org/mailman/listinfo.cgi/boost
>