[contract] extra type requirements for contracts
Hello all, Andrzej and I have been discussing off-line the following issue: How to program contract assertions without adding extra type requirements. I would like to get Boosters' input on possible solutions for this problem. THE PROBLEM Consider the following contract for vector::push_back: CONTRACT_CLASS( template( typename T ) class (myvector) ) { ... CONTRACT_FUNCTION_TPL( public void (push_back) ( (const T&) value ) precondition( size() < max_size(), ) postcondition( auto old_size = CONTRACT_OLDOF size(), auto old_capacity = CONTRACT_OLDOF capacity(), back() == value, // (1) size() == old_size + 1, capacity() >= old_capacity, ) ) ; }; Postcondition (1) introduces the extra requirement EqualityComparable<T>. This is not ideal because this requirement is only needed to check the contract but not to implement the push_back functionality (body). For example: struct pod {}; // not EqualityComparable std::vector<pod> v; v.push_back(pod()); // ok, does not require EqualityComparable<pod> myvector<pod> w; w.push_back(pod()); // complier-error, can't find operator== for type pod... Because of postcondition (1), myvector cannot be used on pod while the std::vector can! This is a general issue with contracts. In general, an arbitrary complex (const) expression can be used to assert preconditions, postconditions, or invariants. Such a complex assertion might introduce an arbitray set of extra requirements on the types used, requirements that might not be necessary to implement the function body. The extra type requirements introduced by the contracts are especially problematic when programming templates because the used types are generic and it is not know a priori to the function programmer if the generic types will or not satisfy the requirements. POSSIBLE SOLUTIONS A possible solution is to specify the type requirements that a given assertion introduces. If the type requirements are met, the assertion will be compiled and checked at run-time. If the type requirements are not met, the assertion will not be compiled (so not compiler-error "missing operator== for type ...") and not checked at run-time for that specific type. For example: CONTRACT_FUNCTION_TPL( // Option 1 public void (push_back) ( (const T&) value ) precondition( size() < max_size(), requires has_less<size_type>::value ) postcondition( auto old_size = CONTRACT_OLDOF size(), requires const_copy_constructor<size_type>::value auto old_capacity = CONTRACT_OLDOF capacity(), requires const_copy_constructor<size_type>::value back() == value, requires has_equal_to<T>::value // assertion type requirements size() == old_size + 1, requires has_equal_to<size_type>::value && has_plus<size_type>::value capacity() >= old_capacity, requires has_greater_equal<size_type>::value ) ) ; Here I have specified assertion type requirements using `requires` for each assertion. However, size_type is known a priori to be essentially an unsigned int for which all these type requirements will always be met so the type requirements on size_type could have been omitted. That said, you can easily imagine an example for a different template class or function where size_type is also a generic type for which const copy constructor, +, ==, etc might not always be available. Another option would be would be to specify the type requirements for precondition/postcondition instead than for each assertion: CONTRACT_FUNCTION_TPL( // Option 2. public void (push_back) ( (const T&) value ) precondition( size() < max_size(), ) requires has_less<size_type>::value // pre/postcondition type requirements postcondition( auto old_size = CONTRACT_OLDOF size(), auto old_capacity = CONTRACT_OLDOF capacity(), back() == value, size() == old_size + 1, capacity() >= old_capacity, ) requires const_copy_constructor<size_type>::value && has_equal_to<T>::value && has_plus<size_type>::value && has_greater_equal<size_type>::value ) ; Options 2 is less verbose and it does not specify the same type requirements multiple time for the different assertions. However, I prefer Option 1 because if T is not equality comparable, only the postcondition `back() == value` is not checked but all the other postconditions are still checked. With Option 2 if one type requirement is not met, then all preconditions/postconditions are not checked causing more bugs to go unobserved. If the re-use of the preprocessor "keyword" `requires` was found confusing because of its different semantics when used with concepts, a different preprocessor "keyword" like `unless` could be used instead: CONTRACT_FUNCTION( // Option 3 template( typename InIter1, typename InIter2, typename OutIter, typename BinOp ) requires( boost::InputIterator<InIter1>, boost::InputIterator<InIter2>, typename CONTRACT_IDENTITY_TYPE(( boost::OutputIterator<OutIter, typename boost::InputIterator<InIter1>::value_type > )), typename CONTRACT_IDENTITY_TYPE(( boost::BinaryFunction<BinOp, typename boost::InputIterator<InIter1>::value_type, typename boost::InputIterator<InIter1>::value_type, typename boost::InputIterator<InIter2>::value_type> )) ) (OutIter) (mytransform) ( (InIter1) first1, (InIter1) last1, (InIter2) first2, (OutIter) result, (BinOp) op ) precondition( contract::trivial::range(first1, last1).valid() ) postcondition( auto return_value = return, return_value == result, unless !has_equal_to<T>::value // use unless ) ) { return std::transform(first1, last1, first2, result, op); } Reflections: a) All these solutions require extensive type traits support to write the contract type requirements (I cannot use concepts because they greedily generate compiler-errors when they are not met). However, I see no way around this: I must be able to check the type requirements (extensively using type traits) in order to disable the assertion compilation and their run-time check. b) All these solutions leave the assertions in the contracts so the contract code retains its self-documentation value even then the assertion checking is disabled because the type requirements are not met. c) N1962, Eiffel, D, A++, and all other Contract Programming references that I have seen do not address the issue of the extra type requirements. I am not sure why... Eiffel has generic types but you can always compare them for equality, for non Void, etc. d) In practice, this might not be a big deal because most of the times old-of is applied to counters (int) and postconditions are the ones introducing the extra requirement but only of EqualityComparable. However, in general I think I need to provide a solution for this issue. What do you think? Thanks a lot! --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
2011/9/19 lcaminiti <lorcaminiti@gmail.com>
Why not use SFINAE expressions to disable post conditions that aren't well-formed? SFINAE expressions feature is required by the C++11 and is available in several C++03 implementations including gcc and MSVC. Roman Perepelitsa.
[Roman Perepelitsa]
SFINAE expressions feature is required by the C++11 and is available in several C++03 implementations including gcc and MSVC.
This is incorrect for VC. I've double-checked with our compiler front-end team - expression SFINAE wasn't actively supported in VC10 (and earlier). It sometimes worked by chance. In VC11, due to other bugfixes, it'll work in more cases but still isn't fully supported. Stephan T. Lavavej Visual C++ Libraries Developer
on Mon Sep 19 2011, lcaminiti <lorcaminiti-AT-gmail.com> wrote:
If the contract can't be expressed within the constraints, the constraints are broken, period. Now, however, the standard contains special hand-wavey language that says, essentially, "when we use a == b to describe a postcondition we don't literally mean ==. We mean that a and b are equivalent" (whatever that means). So even if T supports == it doesn't necessarily mean the standard is going to use it. I think what it really means is that b is indistinguishable from any other copy of a. ...which doesn't help you at all in terms of deciding what to actually /do/, I know... hopefully, though, it muddies the water a bit just in case it was too clear for you up till now ;-) -- Dave Abrahams BoostPro Computing http://www.boostpro.com
Dave Abrahams wrote:
But this means that if you add contracts to vector<T> then you cannot use it unless T is EqualityComparable... I don't think that will be acceptable to Boost.Contract users... will it be acceptable?
I will study this part of the standard. Thanks, --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
on Tue Sep 20 2011, lcaminiti <lorcaminiti-AT-gmail.com> wrote:
No, almost certainly not. It would probably be reasonable to say that *if* T supports ==, the contract checking will use that, and otherwise, the parts of the contract that depend on == won't be checked. Another reasonable possibility (which could be used together with the former one) would be to provide a hook for people to implement some equivalence test for T that isn't spelled "==". That said, I would argue that if they can implement the equivalence test, they should call it "==". Overall I have more confidence in the first idea above than in the second one.
Good luck. Incidentally, this is part of the reason Stepanov puts so much emphasis on the importance of "regular types:" you can't check (programmatically or by inspection) even the most basic assertions about the correctness of code that copies data unless you have some notion of "==" for just about everything. However, the C++ standard was written to accomodate "partial" types that lack essential operations, so what are you gonna do? -- Dave Abrahams BoostPro Computing http://www.boostpro.com
Dave Abrahams wrote:
Yes, this is exactly what the assertion type requirement idea tries to do: CONTRACT_FUNCTION_TPL( // option 1 public void (push_back) ( (T const&) value) postcondition( back() == value, requires has_equal_to<T>::value ) ) ; Here the assertion `back() == value` is compiled and checked if and only if its requirement `has_equal_to<T>::value` is true for T.
Yes, this is what I have currently implemented: namespace dummy { template< typename L, typename R > bool operator== ( L const& left, R const& right) { return true; } } CONTRACT_FUNCTION_TPL( // option 2 public void (push_back) ( (T const&) value) postcondition( using dummy::operator==, back() == value ) ) ; This will use the dummy implementation of operator== only when T does not already have a better match for operator==. Boost.Contract could in fact provide a bunch of dummy operator implementations as contract::trivial::operator==, contract::trivial::operator<, etc. The implementation doesn't have to be dummy, with this method you can actually program a special operator== that does something and to be used by the contract only when T does not already have an operator==. (Note that contracts can safely allow using directives, namespace aliasing, typedefs, etc because these are all constant correct operations as they do not change the program's run-time state.)
Overall I have more confidence in the first idea above than in the second one.
I like option 1 better than option 2 because option 1 is more general while option 2 only handles the == case (and some other predefined operations like <, etc). What do you think?
I think that's why Eiffel does not address the extra type requirement issue because (AFAIK) you can always compare Eiffel's types for equality.
Because Boost.Contract implements Contract Programming for C++, I must deal with the partial types that the C++ standards allows... so I think I will implement option 1 (or option 2) and document that if you don't provide meaningful == most of your assertions (especially postconditions) won't be checked. Thanks a lot! --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
lcaminiti wrote:
Hello all, I am trying to program an assertion that is compiled and checked at run-time only when an integral boolean expression expressing the assertion requirements is true. For example, the following code asserts back() == value only when can_call_equal<T>::value is true. However, is there a better way to do this that does not require the extra function call to post1? #include <boost/mpl/bool.hpp> #include <boost/type_traits/can_call_equal.hpp> #include <vector> #include <cassert> #include <iostream> template< typename T > struct myvector { // CONTRACT_FUNCTION_TPL( // public void (push_back) ( (T const&) value ) // postcondition( // back() == value, requires boost::can_call_equal<T>::value // ) // ) { vector_.push_back(value); } void post1 ( boost::mpl::true_, T const& value ) const { std::clog << "actual assertion\n"; assert( /**/ back() == value /**/ ); } void post1 ( boost::mpl::false_, T const& value ) const { std::clog << "trivial assertion\n"; } void push_back ( T const& value ) { body(value); post1(typename boost::mpl::bool_< /**/ boost::can_call_equal<T>::value /**/ >::type(), value); } void body ( T const& value ) /**/ { vector_.push_back(value); } /**/ T const& back ( void ) const { return vector_.back(); } private: std::vector<T> vector_; }; struct pod {}; int main ( ) { myvector<int> v; std::clog << "push 123\n"; v.push_back(123); myvector<pod> w; std::clog << "push POD\n"; w.push_back(pod()); return 0; } Note that post1(boost::mpl::true_, ...) is not even compiled for myvector<pod> and that is essential because such a compilation attempt will fail because pod does not have an operator==. Thanks a lot for any suggestion you might have. --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
lcaminiti wrote:
Hi, I think you can provide something simpler. Instead of writing the enabling condition maybe you can use an intermediary function. In your case instead of using directly back() == value you can use are_equivalents(back(),value) this function can be defined to use back() == value when boost::can_call_equal. The default definition could be to return true or just don't define it at all and let the user make the specialization. I guess that your macros could replace these automatically, so the user could continue to use back() == value. Best, Vicente -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
Vicente Botet wrote:
I think this can be achieved with my previous "option 2" suggestion: namespace dummy { template< typename L, typename R> bool operator== ( L const&, R const& ) { return true; } } postcondition( using dummy::operator==, back() == value ) This will use T's operator== if there is one, otherwise it will use operator== from the dummy namespace. You can defined/overload the dummy::operator== as you wish (Boost.Contract might even provide a few of such dummy operators as contract::trivial::operator==, contract::trivial::operator<, etc). There is no need for the macros to do anything special here. However, option 2 deals well with the (most common) issue of operator== but it doesn't handle the general issue that an assertion might introduce an arbitrary extra set of type requirements on generic types (e.g., == and + and copyable and ...). So I want to also implement option 1 "assertions with type requirements" P.S. Plus I think I can use option 1 to also implement assertion importance ordering and therefore remove the "importance" keyword: // Use importance ordering (in assertion requirements) to model computational complexity. #define O_1 0 // O(1) #define O_N 1 // O(n) #define COMPLEXITY_MAX O_1 // Only check assertions with constant complexity. postcondition( auto result = return, result == *(std::find(v.begin(), v.end(), value)), requires O_N <= COMPLEXITY_MAX && has_equal_to<T>::value ) Thanks. --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
On Thu, Sep 22, 2011 at 8:03 AM, lcaminiti <lorcaminiti@gmail.com> wrote: [...]
I'm not sure how you can get away *without* conditionally compiling the "back() == value" expression, and since your condition is only known at instantiation time, it seems the only way to effect this is through a function overload or class specialization. What is undesirable about the "extra function call"? #include <boost/mpl/bool.hpp>
Agreed. Again, can you be specific about what the problems with this are? - Jeff
Jeffrey Lee Hellrung, Jr.-2 wrote:
Yes, the issues are (small): 1) It's harder for me to implement the macros to deal with the extra post1 function definition and call (harder but possible, I think). 2) The run-time overhead of the extra post1 function call-- but if you are really concerned about run-time performances, you'd disable contracts (and especially postconditions) anyway by #defining CONTRACT_CONFIG_NO_POSTCONDITIONS, etc. So I guess I just roll up my sleeves and implement the macros to expand the extra function calls ;) but I wanted to check with Boosters if there are alternatives to implement this (BTW, I can only use C++03 features to do this). Thanks a lot! --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
lcaminiti wrote:
Hello all, This is how assertion requirements implementation turned out to be (many thanks again to everyone and especially to Andrzej Krzemienski for your suggestions): #include <contract.hpp> #include <boost/type_traits/can_call_equal.hpp> #include <boost/type_traits/can_call_greater.hpp> #include <boost/concept_check.hpp> #include <boost/utility.hpp> #include <iostream> template< typename T > class PreIncrementable { T& x; void return_type ( T& ); public: BOOST_CONCEPT_USAGE(PreIncrementable) { return_type(++x); } }; CONTRACT_FUNCTION( template( typename T ) requires( PreIncrementable<T> ) (T&) (inc) ( (T&) value ) postcondition( auto result = return, // skip this old-of copy if `has_oldof<T>::value` is false auto old_value = CONTRACT_OLDOF value, // skip this assertion if `has_oldof<T>::value` is false value > old_value, // also skip if T has no operator> requires contract::has_oldof<T>::value && // need old-of boost::can_call_greater<T>::value, // need > result == value, // skip this assertion if T has no operator== requires boost::can_call_equal<T>::value // need == ) ) { return ++value; } struct counter : boost::noncopyable { // cannot copy (for some reason...) counter ( ) : number_(0) {} counter& operator++ ( ) { ++number_; return *this; } friend bool operator> ( counter const& left, counter const& right ) { return left.number_ > right.number_; } void print ( ) { std::cout << number_ << std::endl; } private: int number_; }; // specialization disables old-of for non-copyable `counter` (no type trait can // be implemented in C++ to automatically and portably detect copy constructor) namespace contract { template<> struct has_oldof<counter> : boost::mpl::false_ {}; } int main ( ) { int i = 0; std::cout << inc(i) << std::endl; // check entire contract for `int` type counter c; inc(c).print(); // cannot copy `counter` so skip assertion with old-of return 0; } Unfortunately, some extra work is required by the users to deal with old-of -- they need to specialize has_oldof. This is because there is no type trait that can check if a type T has a const-correct copy constructor (portably and also including user-defined copy constructors) so I was forced to trivially inherit has_oldof<T> from mpl::true_ (this way contract compilation will fail for types without a const-correct copy constructor and in this case programmers can specialize has_oldof to inherit from false_ to disable the old-of assertions and compile the code as in the example above). To be precise, my library copies old-of using a copy<> template which by default looks for a const-correct copy constructor. So users have full control even if they want old-of for a type that cannot define a const-correct copy constructor by specializing both copy<> and has_oldof<> (but this is a rather advanced use of the library and it is probably never needed). All of that said, usually old-of copies are takes for counters or iterators so you don't even have to worry about specifying the has_oldof requirements in the contracts (let alone specializing has_oldof) because these types will always be copyable. --Lorenzo -- View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-fo... Sent from the Boost - Dev mailing list archive at Nabble.com.
participants (6)
-
Dave Abrahams -
Jeffrey Lee Hellrung, Jr. -
lcaminiti -
Roman Perepelitsa -
Stephan T. Lavavej -
Vicente Botet