On Mon, 18 May 2015, Jacob Sparre Andersen wrote:

> Stefan.Lucks@uni-weimar.de wrote:
>
>> Thirdly, even if it would be way too expensive to check this
>> specification at run time, it may be possible to verify it statically
>> at run time. But I can only find that out by writing the specification
>> and then running my tool (the compiler or whatever). Again, it would
>> be a terrible idea for the compiler to insert expensive checks just
>> because the theorem prover failed to prove the condition.
>
> Why?  Wouldn't it be better to have the check enabled by default, and
> only disable it once profiling has shown that it is prohibitively
> expensive?

Well, as a very simmple example, consider this:

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

You don't need a profiler to figure out that this is prohibitively slow 
for largish N, do you?

> I am aware that we currently don't have as fine-grained control of 
> assertions as that would require to work well, but I assume that this is 
> something that can be discussed with the ARG and the compiler vendors.

This is precisely my point!

Stefan

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