Re: {Pre,Post}conditions and side effects

["G.B." <bauhaus@futureapps.invalid>]

On 09.06.15 09:55, Stefan.Lucks@uni-weimar.de wrote:
> On Tue, 19 May 2015, Jacob Sparre Andersen wrote:
>
>> Stefan.Lucks@uni-weimar.de writes:
>>>
>>>     (for all I in 2 .. N-1 => (N mod I) /= 0)
>>>
>> I don't need a profiler to estimate that it takes long time to execute,
>> but I need a profiler to see where the compiler can't eliminate it from
>> a critical path through static analysis.
>
> Sorry, i forgot about this thread ... so my response is somewhat late.
>
> If N is large enough, the compiler would have to eliminate that
> expression from all paths, not just from its critical path. (Think of N
> \approx 2**60. Which comes first: your program passing or failing all
> test cases, or your retirement?)
>
>> Good.  I noticed an interesting proposal for an extension to the
>> assertion policy control in one of the posts in this thread.  I suppose
>> we should push to have the ARG accept this (or something similar).
>
> Agreed!

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));

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. The latter could be considered off-topic the more it reflects
a project's own vocabulary, which cannot be as universally familiar
as a quantified_expression.

Does Config belong in a contract?

Moreover, aspects that allow one to address the issue at the language
level, outside the contract, not using mere conventions, would be more
standard, and meet standard expectations. Somewhat like contracts always
define things and state when a thing does apply, and to what.

These aspects and the notion of configuration do not need
to exclude each other, if the words Configuration Pragma imply that.