Re: [boost] [contract] Contract Programming Library
Andrzej Krzemienski
> Design By Contract (TM) ) for C++.
> I have drafted some of the library documentation in Boost-like format:
> http://dbcpp.sourceforge.net/boost/libs/contract/doc/html/
> Comments?
Hi,
I would be very interested in trying such a library. I have one
suggestion, which may be impossible to implement, but I think it would
be worth at least looking at.
The macros for defining assertions spoil function declarations. I know
it is inevitable, etc., but.. read on. I know at least one library in
Boost that also spoils function declarations in order to provide
additional functionality: Concept Check library; they may be others
too (MPL?).
My suggestion is that if there are (or will be) libraries that require
spoiling function declarations, they should all provide the same
"spoiled" syntax. Otherwise I will be always asking "how do I declare
a function in this library?". It would be very convenient if Boost
provided one alternative function definition syntax that when used
would enable all its libraries to work.
Regards,
&rzej
_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Lorenzo Caminiti
On Fri, Feb 12, 2010 at 3:39 AM, Andrzej Krzemienski <akrz...@gmail.com> wrote:
> I would be very interested in trying such a library. I have one
I am updating the documentation then I will release the library on
SourceForge (as Contract++ not as Boost.Contract) for everyone to try
it. I hope I will receive feedback!
> it is inevitable, etc., but.. read on. I know at least one library in
> Boost that also spoils function declarations in order to provide
> additional functionality: Concept Check library; they may be others
> too (MPL?).
> My suggestion is that if there are (or will be) libraries that require
> spoiling function declarations, they should all provide the same
> "spoiled" syntax. Otherwise I will be always asking "how do I declare
> a function in this library?". It would be very convenient if Boost
> provided one alternative function definition syntax that when used
> would enable all its libraries to work.
I agree. However, in the past I did look into harmonizing my library
API with the ones of Boost.ConceptCheck and/or Boost.Parameter but it
did not seem feasible... I will double check it.
Regards,
Lorenzo
Andrzej Krzemienski
> Design By Contract (TM) ) for C++.
> I have drafted some of the library documentation in Boost-like format:
> http://dbcpp.sourceforge.net/boost/libs/contract/doc/html/
> Comments?
Hi,
I have a couple of questions/suggestions regarding the documentation
of the library.
(1)
Does it execute postconditions when the function body ends with a
thrown exception? Obviously it shouldn't. I can see one lie saying
It is possible to describe the function postconditions.
These are logical conditions that programmers expect
to be true when the function has ended **normally**.
So I guess it doesn't, but I believe this fact deserves some more
room in the documentation, like "public member function is not
required to satisfy the postcondition if it ends with exception."
(2)
Obviously, the expressions in assertions shouldn't change the
behaviour of the program when executed. This requirement is stronger
than having no side effects. You protect the object itself by allowing
only const member functions. Are the function arguments (those passed
by mutable reference also protected?).
Is it allowed/recommended to refer to global or static data in the
assertions? If you are using clever macros, perhaps there is a way to
block the references to these. In C++0x lambdas you can specify a list
of objects you want to refer to:
[this, &max_value, &count, &cache]( int fact1, int fact2 ) {...}
perhaps there is a way to do it with current C++ macros.
(3)
In a similar manner, what happens if one of postcondition's assertions
throws an exception? I have troubles answering this question myself (I
do not know what should ideally happen), but whatever your answer is,
I believe it should be clearly documented. (Note that this is not only
the issue of DbC; simple C-assertions also leave this question
unanswered).
(4)
Do the assertions have access to objet's private/protected interfaces?
(I believe they shouldn't).
(5)
Does the library allow defining preand postconditions for "free"
functions or static member functions? The examples are so focused on
objects/classes that I cannot tell the answer.
(6)
Similarly, does the library allow defining block invariants?
(7)
The documentation lists the following sequence for executing a constructor:
1. Initialize member variables via the constructor member
initialization list (if such a list is specified).
2. Check preconditions (but not invariants).
3. Execute constructor body.
4. Check invariants.
5. Check postconditions.
I believe, one of the reasons for validating arguments of a constuctor
is to not allow the incorrect values to initialize objest's
sub-objects (members). I believe the sequence of the first two items
should be inverse. Am I wrong?
(8)
Since library usses macros that make the syntax a bit difficult to
read/parse, perhaps it would be useful to augment every example with
another one that would say how the same thing would be acomplished
with fictitious "DbC C++" syntax if we had one. This was done for
Boost Interface library (under construction,
http://www.cdiggins.com/bil.html) and I think it helps a lot.
Regards,
&rzej
Andrzej Krzemienski
two other questions that came to my mind, regarding the library design.
(1)
Sometimes the assertions execute longer than the function itself. For example:
iterator find( iterator begin, iterator end, value v )
precondition { is_sorted( begin, end ); }
{
return find_sorted( begin, end, v );
}
find_sorted has logarithmic complexity, whereas is_sorted has linear
one. If I use function find like this:
sort( begin, end );
process( find(begin, end, A) ); // call is_sorted
process( find(begin, end, B) ); // call is_sorted
process( find(begin, end, C) ); // call is_sorted
is_sorted is called many a time. Even if I am in debugging mode but
use a medium size range, the performance can kill me. I would like to
disable checking of this assertion, but at the same time there is no
reason to disable others. Would you consider providing a way to
selectively disable asserts? some assertion level?
(2).
Usually public member functions would be used to express DbC
assertions. Do you disable assertions in public functions that are
called only to evaluate other assertions in order to avoid recursive
calls?
Andrzej Krzemienski
> > Boost that also spoils function declarations in order to provide
> > additional functionality: Concept Check library; they may be others
> > too (MPL?).
> > My suggestion is that if there are (or will be) libraries that require
> > spoiling function declarations, they should all provide the same
> > "spoiled" syntax. Otherwise I will be always asking "how do I declare
> > a function in this library?". It would be very convenient if Boost
> > provided one alternative function definition syntax that when used
> > would enable all its libraries to work.
>
> I agree. However, in the past I did look into harmonizing my library
> API with the ones of Boost.ConceptCheck and/or Boost.Parameter but it
> did not seem feasible... I will double check it.
This is not only about clarity. As a super-correct programmer I may want to
apply both concept checking and pre-/post-conditions checking to my functions.
Perhaps, if the 'compromise' syntax is possible, it requires changing
concept-checking library.
Lorenzo Caminiti
Most of your questions are answered by the documentation updates I am
making now. Please see my "preview" answers below.
Note that some of the points you make are "policy" decisions. I listed
what the library currently does, but a different "policy" could be
implemented easily within the library.
On Tue, Feb 16, 2010 at 4:34 AM, Andrzej Krzemienski <akrz...@gmail.com> wrote:
> Hi,
> I have a couple of questions/suggestions regarding the documentation
> of the library.
>
> (1)
> Does it execute postconditions when the function body ends with a
> thrown exception? Obviously it shouldn't. I can see one lie saying
>
> It is possible to describe the function postconditions.
> These are logical conditions that programmers expect
> to be true when the function has ended **normally**.
>
> So I guess it doesn't, but I believe this fact deserves some more
> room in the documentation, like "public member function is not
> required to satisfy the postcondition if it ends with exception."
No, postconditions are NOT checked if the body throws. However, class
invariants are checked also when the body throws (requirement from
[Crowl2006], see library documentation bibliography).
> (2)
> Obviously, the expressions in assertions shouldn't change the
> behaviour of the program when executed. This requirement is stronger
> than having no side effects. You protect the object itself by allowing
> only const member functions. Are the function arguments (those passed
> by mutable reference also protected?).
Object, all function arguments, and result value are passed as
constant references. This is true even if the contracted function is
not a constant member, it has non const& arguments, and non const&
result (the const& is added using Boost.TypeTraits).
> Is it allowed/recommended to refer to global or static data in the
> assertions? If you are using clever macros, perhaps there is a way to
> block the references to these. In C++0x lambdas you can specify a list
> of objects you want to refer to:
> [this, &max_value, &count, &cache]( int fact1, int fact2 ) {...}
> perhaps there is a way to do it with current C++ macros.
Assertions appear in constant member function so the can access static
data, etc as usual.
I need to study the rest of your comment above C++(0x lambdas) more...
> (3)
> In a similar manner, what happens if one of postcondition's assertions
> throws an exception? I have troubles answering this question myself (I
> do not know what should ideally happen), but whatever your answer is,
> I believe it should be clearly documented. (Note that this is not only
> the issue of DbC; simple C-assertions also leave this question
> unanswered).
If code checking the contract (invariants, preconditions,
postconditions) throws any exception the contract is considered failed
and the relative failure handler function is invoked (default
std::terminate() but can be redefined by the user). This is because if
it is not possible to check that a contract condition is true, due to
an exception, then the only "safe" thing to do is to assume that the
asserted condition failed.
> (4)
> Do the assertions have access to objet's private/protected interfaces?
> (I believe they shouldn't).
Yes, any public/protected/private member can be accessed by the contracts.
Preconditions should only access public members (otherwise the callers
cannot fully check them) and Eiffel enforces this at compile-time.
However, my library does not enforce this constraint and leaves it up
to programmers to write good preconditions that do not use protected
or private members. (Due to C++ friendship it is somewhat difficult to
fully embrace the argument that preconditions should not access
private members in C++ because even if they do callers that are
friends of the class can still check them...)
Class invariants and postconditions can access non-public members
(also in Eiffel) as their contracts are allowed to the check the
correctness of the implementation (for example invariants assert a
private member pointer is always not null).
In general, I find assertions that use public members to be much more
useful because they are the ones documenting the specifications (not
the implementation).
> (5)
> Does the library allow defining preand postconditions for "free"
> functions or static member functions? The examples are so focused on
> objects/classes that I cannot tell the answer.
Yes (just implemented and documented).
> (6)
> Similarly, does the library allow defining block invariants?
Yes (just implemented and documented). The library supports block
invariants (which can also be used to assert loop invariants) as
specified in [Crowl2006]. Also Eiffel-like loop variants are
supported.
void f(std::vector v, const size_t& n) {
size_t i = 0;
CONTRACT_ASSERT_BLOCK_INVARIANT( i == 0 );
for (CONTRACT_INIT_LOOP_VARIANT; i < v.size(); ++i) {
}
> (7)
> The documentation lists the following sequence for executing a constructor:
>
> 1. Initialize member variables via the constructor member
> initialization list (if such a list is specified).
> 2. Check preconditions (but not invariants).
> 3. Execute constructor body.
> 4. Check invariants.
> 5. Check postconditions.
>
> I believe, one of the reasons for validating arguments of a constuctor
> is to not allow the incorrect values to initialize objest's
> sub-objects (members). I believe the sequence of the first two items
> should be inverse. Am I wrong?
The library follows Eiffel semantics for constructor which is {Default
AND Pre}Body{Post AND Inv} where Default is default initialization of
members (similar to C++ member initialization list). That said, it
would be difficult to implement a different semantics (like the one
you suggest) in C++ because of the lack of delegating constructors.
> (8)
> Since library usses macros that make the syntax a bit difficult to
> read/parse, perhaps it would be useful to augment every example with
> another one that would say how the same thing would be acomplished
> with fictitious "DbC C++" syntax if we had one. This was done for
> Boost Interface library (under construction,
> http://www.cdiggins.com/bil.html) and I think it helps a lot.
The documentation shows the macros (in Tutorial), the expanded code
(in Without the Macros), and it refers to [Crowl2006] for how language
support would look like. But I will look into your suggestion (I will
study Boost.Interface).
Lorenzo Caminiti
Sorry, I realize I did not complete the loop example:
void f(std::vector v, const size_t& n) {
size_t i = 0;
CONTRACT_ASSERT_BLOCK_INVARIANT( i == 0 ); // Block inv.
for (CONTRACT_INIT_LOOP_VARIANT; i < v.size(); ++i) {
CONTRACT_ASSERT_BLOCK_INVARIANT( i < v.size() ); // Block inv
as loop inv.
CONTRACT_ASSERT_LOOP_VARIANT( v.size() - i ); // Loop variant.
...
}
}
On Tue, Feb 16, 2010 at 3:01 PM, Andrzej Krzemienski <akrz...@gmail.com> wrote:
> use a medium size range, the performance can kill me. I would like to
> disable checking of this assertion, but at the same time there is no
> reason to disable others. Would you consider providing a way to
> selectively disable asserts? some assertion level?
Yes, I will consider this in the future. Also, I might want to check
inv/pre/post for most of the classes I compile but not for a few
templates part of a library that I trust (e.g., Boost). So it would be
nice to select different contract checking levels (at least at
run-time) based on class name or similar.
> (2).
> Usually public member functions would be used to express DbC
> assertions. Do you disable assertions in public functions that are
> called only to evaluate other assertions in order to avoid recursive
> calls?
Yes, the library policy is to disable assertion checking within
assertions and to disable class invariants checking for nested
function calls (public or not) (requirements from [Meyer1997],
[Ottosen2004], and [Crowl2006]). Different policies could be
implemented but this one avoids infinite recursion well in my
experience.
Regards,
Lorenzo
Andrzej Krzemienski
> >
> > 1. Initialize member variables via the constructor member
> > initialization list (if such a list is specified).
> > 2. Check preconditions (but not invariants).
> > 3. Execute constructor body.
> > 4. Check invariants.
> > 5. Check postconditions.
> >
> > I believe, one of the reasons for validating arguments of a constuctor
> > is to not allow the incorrect values to initialize objest's
> > sub-objects (members). I believe the sequence of the first two items
> > should be inverse. Am I wrong?
> The library follows Eiffel semantics for constructor which is {Default
> AND Pre}Body{Post AND Inv} where Default is default initialization of
> members (similar to C++ member initialization list). That said, it
> would be difficult to implement a different semantics (like the one
> you suggest) in C++ because of the lack of delegating constructors.
The sole fact that other language implements it this way is not
sufficient an argument. I can think of the situation when "Eiffel
order" may cause damage that the inverse order might have prevented:
Type::Type( int & counter )
precondition{ counter < MAX; }
: handle( irreversibleChange(int--) )
{
;
}
Suppose the constructor of Type is called, and the value of counter is
MAX. This value is invalid, but by the time the precondition is
checked, the irreversibleChange is executed, and the value of counter
is reduced, so the assertion concludes that everything is fine. Now,
the argument that it is difficult to implement is convincing; it may
be that it is impossible at all. But I would call not having the
{Pre->Init} order a limitation of the library. Let me be clear: one
tiny limitation in the great library, because out of many attempts to
provide contract programming to C++ I have seen, this is the only one
that really looks good.
Regards,
&rzej
Lorenzo Caminiti
On Fri, Feb 19, 2010 at 1:16 PM, Andrzej Krzemienski <akrz...@gmail.com> wrote:
> The sole fact that other language implements it this way is not
> sufficient an argument. I can think of the situation when "Eiffel
> order" may cause damage that the inverse order might have prevented:
>
> Type::Type( int & counter )
> precondition{ counter < MAX; }
> : handle( irreversibleChange(int--) )
> {
> ;
> }
>
> Suppose the constructor of Type is called, and the value of counter is
> MAX. This value is invalid, but by the time the precondition is
> checked, the irreversibleChange is executed, and the value of counter
> is reduced, so the assertion concludes that everything is fine. Now,
> the argument that it is difficult to implement is convincing; it may
> be that it is impossible at all. But I would call not having the
> {Pre->Init} order a limitation of the library. Let me be clear: one
> tiny limitation in the great library, because out of many attempts to
> provide contract programming to C++ I have seen, this is the only one
> that really looks good.
I understand your point. Let me spend a few more words on the issue.
1) The library has a limitation in dealing with constructor
initialization lists already. The one limitation currently known and
_documented_ is that if a construct uses member initialization list,
the constructor body definition cannot be separated from the body
declaration (as long as you want to code to still compile when
contract compilation is turned off completely). I have looked at this
limitation and it appears to me that if delegating constructors were
to be supported by C++ as proposed in [Sutter2005] then the library
*could* be able to overcome the limitation (but I cannot really be
sure until I try it...).
2) I think, implementing {Pre AND Default} instead of {Default AND
Pre} without delegating constructors would raise very similar issues
as for 1). Eiffel requirements is {Default AND Pre} but constructors
in Eiffel are different from C++ so your are correct that I should not
simply "copy" the Eiffel requirement if it does not make sense for
C++.
3) If irreversibleChange(count--) could be performed by the
constructor body (instead of the member initialization list, maybe
handle is set to 0 by the initialization list...) then the
preconditions will be checked before irreversibleChange(count--).
However, I understand that for some code maybe the
irreversibleChange(count--) call really has to happen in the member
initialization list... In short, could the code be restructured to
call irreversibleChange(count--) from within the body of a
constructor/function/etc? However, this would be a workaround to the
library limitation that {Pre AND Default} cannot be supported
(limitation which should be documented).
In summary, I will study {Pre AND Default} more. I will look in detail
at why Eiffel does {Default AND Pre}. Also, [Crowl2006] requires:
"Constructors behave much like member functions. This means that a
constructor can have a precondition and a postcondition. The
precondition may not reference member variables." (from [Crowl2006])
but I will also look at all older revisions of this proposal to see if
member initialization list requirements are explicitly mentioned. If
this {Pre AND Default} is the best requirement for C++ Contract
Programming, I will document {Default AND Pre} as a library limitation
(and if not, I will document why {Default AND Pre} is good).
Thank you for your valuable comments.
Lorenzo