[contract] Template types

29 Jul 2016

      Hello all,

I would like to discuss the extra type requirements that contracts can
impose of generic types and how Boost.Contract handles that. I think I
mentioned some of this already in different emails to this list, but I
wanted to summarize this topic in one email.

For example, note that the following code will not compile when the
old value template parameter T is not copyable:

    template<typename T>
    void swap(T& a, T& b)
        [[ensures: a == old(b)]]
        ...

In Boost.Contract (approach 1):

    template<typename T>
    void swap(T& a, T& b) {
        boost::contract::old_ptr<T> old_b = BOOST_CONTRACT_OLDOF(b);
        boost::contract::guard c = boost::contract::function()
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(a == *old_b);
            })
        ;
        ...
    }

In some cases, that might be what the contract writers want: the
generic old value type T is not copyable so postconditions cannot be
checked and the program should not compile. However, in some other
cases the contract writes might not want to add the extra copyable
requirement on T and check the related postconditions only when
callers specify a template parameter T that happens to be copyable.
That can be done allowing some sort of static-if in contracts:

    template<typename T>
    void swap(T& a, T& b)
        [[ensures: static if(is_copyable<T>::value) a == old(b)]]
        ...

In Boost.Contract (approach 2):

    template<typename T>
    void swap(T& a, T& b) {
        boost::contract::old_ptr_if_copyable<T> old_b = BOOST_CONTRACT_OLDOF(b);
        boost::contract::guard c = boost::contract::function()
            .postcondition([&] {
                if(old_b) BOOST_CONTRACT_ASSERT(a == *old_b);
            })
        ;
        ...
    }

Both approach 1 and 2 above are valid and should be supported by the
framework. The decision between which approach to use for a specific
contract should be left up to the programmers.

Like old values can introduce the extra copyable type requirement, any
contract assertion can in general introduce an number of extra
requirements on generic types, namely the type requirements necessary
to support the operations used to program the contract assertions. For
example, the following code will not compile if T is not equality
comparable (which is not a type requirement vector normally imposes on
T):

    template<typename T>
    class vector {
        void push_back(T const& value)
            [[ensures: back() == value]]
            ...
    };

In Boost.Contract (approach 1):

    template<typename T>
    class vector {
        void push_back(T const& value) {
            boost::contract::guard c = boost::contract::public_function(this)
                .postcondition([&] {
                    BOOST_CONTRACT_ASSERT(back() == value);
                })
            ;
            ...
        }
    };

Again, that might be what contract writes want in some case but in
other cases they might want to just skip the assertion when T does not
meet all the type requirements needed by the operations used in the
assertion:

    template<typename T>
    class vector {
        void push_back(T const& value)
            [[ensures: static if(has_equal_to<T>::value) back() == value]]
            ...
    };

In Boost.Contract (approach 2):

    template<typename T>
    class vector {
        void push_back(T const& value) {
            boost::contract::guard c = boost::contract::public_function(this)
                .postcondition([&] {
                    BOOST_CONTRACT_ASSERT(
                        boost::contract::check_if<has_equal_to<T>::value >(
                            boost::bind(equal_to<T>, cref(back()), cref(value))
                        )
                    );
                })
            ;
            ...
        }
    };

--Lorenzo

Lorenzo Caminiti

tags

participants (1)