On Sat, Mar 20, 2010 at 6:54 AM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
OPTION 1: The function declaration is programmed using the usual C++ syntax just before the CONTRACT_FUNCTION() macro.
template<typename T> class myvector {
CONTRACT_INVARIANT( ({ ... }) )
public: void push_back(const T& element) // Usual C++ push_back() declaration. CONTRACT_FUNCTION( (class) (copyable)(myvector) (public) (void) (push_back)( (const T&)(element) ) (precondition)({ ... }) (postcondition)({ ... }) (body)({ ... }) )
... };
OPTION 2: The CONTRACT_FUNCTION() macro automatically programs also the function declaration.
template<typename T> class myvector {
CONTRACT_INVARIANT( ({ ... }) )
public: // No usual C++ push_back() declaration here. CONTRACT_FUNCTION( (class) (copyable)(myvector) (public) (void) (push_back)( (const T&)(element) ) (precondition)({ ... }) (postcondition)({ ... }) (body)({ ... }) )
... };
The OPTION 1 example looks nicer, simply because there's a separate, "classic" C++ declaration before that weird CONTRACT_FUNCTION macro. Someone completely ignorant of Boost.Contract might not want to take the trouble of learning everything, and the (void) (push_back)((const T&) (element) )declaration in OPTION 2 might be skipped because it's right after all those (class)(copyable) etc. etc. because it looks too similar to them (and someone scanning and skipping over CONTRACT_FUNCTION might skip over them). Sincerely, AmkG