Re: [Boost-users] [boost] [contract] static_assert in contracts or not?

Subject: Re: [Boost-users] [boost] [contract] static_assert in contracts or not?
From: Vicente J. Botet Escriba (vicente.botet_at_[hidden])
Date: 2012-08-30 19:49:37

Le 30/08/12 20:13, Lorenzo Caminiti a écrit :
> 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.
Don't forget, that your library is providing some kind of concepts 
interface. I'm wondering if the expression of an static assertion should 
not be moved to the requires part as a constraint of the interface.
>
> 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
>          }
>      {
>          // ...
>      }

What about

     template< typename To, typename From >
         requires {
             sizeof(To) >= sizeof(From) &&
             boost::is_convertible<From, To>
         }
     To* memcopy ( To* to, From* from )
         precondition{
             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");
>          // ...
>      }
IMO these static constraints have no sense as postcondition, as they are 
static. Moving them to the requires should solve the issue.

>
> 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...)
Not yet, but we have enable_if. In addition you are using 
Boost.ConceptCheck on the requires part, that IIUC are not disabled when 
disabling pre/post conditions.
>
> 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.
>
>
No. static assertions must be checked always and at compile time.

Lorenzo, I'm sure that you will be able to extend the requires syntax so 
that we can state static assertions whithout too much effort. E.g. 
something like

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

Best,
Vicente