2 Apr
2010
2 Apr
'10
7:52 p.m.
Hi,
On Sat, Mar 20, 2010 at 10:34 AM, Lorenzo Caminiti
<lorcaminiti@gmail.com> wrote:
> On Tue, Mar 16, 2010 at 6:54 PM, vicente.botet <vicente.botet@wanadoo.fr> wrote:
>> I was wondering if instead of repeating the fuction signature and the class 'signature'
>> you could be able to provide a macro CONTRACT_FUNCTION2 that allows to just write
>> #define CONTRACT_CLASS (class) (myvector) (inherit)(pushable<T>)
>> CONTRACT_FUNCTION2(
>> ((public) (void) (push_back)( (const T&)(element) ))
>
> I have experimented with this a similar idea in the past. However, I
> concluded that copyable class type and inheritance both need to be
> specified at the function-contract level (not at the class-contract
> level) because:
I was able to implement the CONTRACT_CLASS() macro with an interface
similar to what Vicente suggested.
I think this was an important improvement because:
1) Programmers no longer need to repeat the class and base classes
types within CONTRACT_FUNCTION() for every function. The class and
base classes types are only specified once within CONTRACT_CLASS().
2) Perhaps more importantly, now the library is able to
_automatically_ inspect the base classes to see if a specific function
should subcontract or not. This way programmers of derived classes can
no longer "cheat" avoiding to subcontract by omitting (inherit) in
CONTRACT_FUNCTION() -- in fact, (inherit) is gone all together from
the library API.
The myvector example of the documentation
http://dbcpp.sourceforge.net/index.html#contract__.introduction.an_example
now becomes:
#include "pushable.hpp"
#include <contract.hpp>
#include <vector>
template<typename T>
class myvector: public pushable<T> {
CONTRACT_CLASS( (myvector) (pushable<T>) /***** Class and base
classes specified here and only once *****/
(invariant) ({ // For static class invariants use `(static)
(invariant) ({ ... })`.
CONTRACT_ASSERT( (size() == 0) == empty() );
}) )
public:
void push_back(const T& element)
CONTRACT_FUNCTION( /***** No class and no (inherit) here anymore *****/
(public) (void) (push_back)( (const T&)(element) )
(copyable) /***** Copyable qualifier for the object is moved at the
end of the function signature (same as cv-qualifier) *****/
(precondition)({
CONTRACT_ASSERT( size() < max_size() );
})
(postcondition)({
CONTRACT_ASSERT( size() == (CONTRACT_OLDOF(this)->size() + 1) );
})
(body)({
vector_.push_back(element);
}) )
typedef typename std::vector<T>::size_type size_type;
size_type size(void) const { return vector_.size(); }
size_type max_size(void) const { return vector_.max_size(); }
bool empty(void) const { return vector_.empty(); }
const T& back(void) const { return vector_.back(); }
private:
std::vector<T> vector_;
};
Note that the (copyable) object qualifier is still specified at
function scope because for the same class a function might need
CONTRACT_OLDOF(this) in its postconditions while another might not. I
have decided to specify the (copyable) object qualifier at the end of
the function signature so to follow a similar syntax as for the
cv-qualifier "(const)/(volatile)/(copyable) at the end of a member
function signature qualify the object as const/volatile/copyable
within that member function".
>From an implementation prospective:
1) CONTRACT_CLASS() defines typedefs for the class and base classes
types with predefined names so that CONTRACT_FUNCTION() knows how to
access them.
2) CONTRACT_FUNCTION() expands to code that uses uses SFINAE to
inspect the base class types looking for the struct which defines the
function contract (see the "[has_function]" email thread).
3) The function contract struct has a unique name for a given function
within a class plus it differentiates if a base function is virtual or
not.
This way the library can automatically subcontract x::f() from the
contract of y::f() only if y is a base of x, and y is virtual, and
y::f() has a contract.
Thanks a lot for the suggestion.
Lorenzo