[boost] [contract] static_assert in contracts or not?

Subject: [boost] [contract] static_assert in contracts or not?
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-08-30 14:13:53

Hello all,

If static assertions make sense within contracts (preconditions,
postconditions, and class invariants) is a questions that has been
raised by both Vicente and Andrzej. I don't have a definitive answer
so I'd like to discuss with the ML.

On Wed, Aug 29, 2012 at 2:48 PM, Andrzej Krzemienski <akrzemi1_at_[hidden]> wrote:
> (6)
> Static assertions: is there any value in providing them, given that we
> already have this ability in Boost? I see that N1962 decided to abandon
> them; I am pretty sure the reason was that static_assert was already there.
> They somehow do not fit conceptually into the model of preconditions,
> postconditions and invariants. Precondition, for instance tries to detect a
> run-time condition occurring immediately before a function is called this
> time. Static assertion is not even executed then. What point is there in
> putting such assertion into the precondition? Documentation says " static
> assertions can be selectively disabled depending on where they are
> specified [...] so it is still important to logically associate them with
> preconditions, postconditions, etc." -- technically this sentence makes
> logical sense, but can you think of a single example where this selective
> disabling of assertions would be useful? What is the point in disabling
> such assertions at all, if they cost you nothing in run-time? I propose to
> remove them and give a sort of recommendation that software quality is
> assured by using a number of fairly independent tools: DbC, concepts,
> static assertions.

I think we can break down the question in two parts. Let's assume
N1962 is accepted into C++1x so we have both contracts and
static_assert.

1) Would you expect to be able to use static_assert within contract
assertions (preconditions, postconditions, and class invariants)? Note
that only boolean conditions are allowed by N1962 within contracts,
general code is not allowed, therefore this is not a trivial question.

For example, would you expect to be able to do the following option A:

    template< typename To, typename From >
    To* memcopy ( To* to, From* from )
        precondition{
            static_assert(sizeof(To) >= sizeof(From), "destination too small");
            static_assert(boost::is_convertible<From, To>::value,
"incompatible types");
            to; // pointer not null
            from; // pointer not null
        }
    {
        // ...
    }

In this case, would it ever make sense to use static_assert in
postcondition and/or class invariants even if that were allowed?

Or would you just use static_assert in the body, option B:

    template< typename To, typename From >
    To* memcopy ( To* to, From* from )
        precondition{
            to; // pointer not null
            from; // pointer not null
        }
    {
        static_assert(sizeof(To) >= sizeof(From), "destination too small");
        static_assert(boost::is_convertible<From, To>::value,
"incompatible types");
        // ...
    }

I don't like this because the assertions are about the specifications
(they assert a requirement of the interface) so they should go in the
declaration and not in the implementation.

Or maybe the assertions should be represented as concept requirements
on To and From, option C:

    template< typename To, typename From >
        requires SizeofGreaterEqual<To, From>, Convertible<From, To>
    To* memcopy ( To* to, From* from )
        precondition{
            to; // pointer not null
            from; // pointer not null
        }
    {
        // ...
    }

(Only we don't have concepts...)

2) Let's assume, we answered option A to question 1):

    template< typename To, typename From >
    To* memcopy ( To* to, From* from )
        precondition{
            static_assert(sizeof(To) >= sizeof(From), "destination too small");
            static_assert(boost::is_convertible<From, To>::value,
"incompatible types");
            to; // pointer not null
            from; // pointer not null
        }
    {
        // ...
    }

Would you expect these static_asserts to be disabled when precondition
compilation and checking is turned off at compilation time? I'd think
so.

Thanks.
--Lorenzo