On Tue, 9 Jun 2015, G.B. wrote:

> It has been suggested in some places that assertion control
> should be exercised with the help of a Config package.
>
>   with $Condition$ =>
>       (if Config.Is_Expensive_Test_666 (N)
>        then True
> 	else (for all I in 2 .. N-1 => (N mod I) /= 0));

On one hand, it is cool that the syntax for contracts is sufficiently 
flexible to allow this kind of thing, On the other hand, this is a plain 
abuse of the syntax for contracts, and it significantly decreases the 
contract's readability, because the real meaning is just

    $Condition$ =>
       (for all I in 2 .. N-1 => (N mod I) /= 0)

while the rest *could* be misunderstood as "under certain circumstances,
the above condition doesn't need to hold", rather than "this condition 
must always hold, even though it is not always checked or verified".

> While it was considered practical, maybe even charming because Config
> is just Ada, allowing to choose configuration names, permitting
> conditional conditions (cf. N above), it would inevitably introduce
> idiosyncrasies and, more importantly IMO, shift attention to Config
> stuff.

Indeed!

A somewhat lightweigt extension of the Ada 2012 syntax could allow 
$Condition$(Boolean_Expression), with $Condition$(True) being the same 
as $Condition$, e.g.:

   pre(False) => -- require this, but never check
     (for all I in 2 .. N-1 => (N mod I) /= 0),

   pre(Testing_Level >= Minimum ) =>
    ((N mod 2 /= 0) and then (N mod 3 /= 0));

   pre(Testing_Level >= High) => -- checked during nightly tests
     (for all I in 5 .. Num_Type'Min(2**32, N-1) => (N mod I) /= 0)),



------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--