On Tue, 12 May 2015, Stefan.Lucks@uni-weimar.de wrote:

>>> So the above specifies properly what I want to have. But this is also
>>> terribly slow.
> [...]
>>> I.e., this is a valid specification, but a useless test.
>> 
>> Correct. If it hurts, don't write that. :-)

> Secondly, the compiler or prover may need need such "believe me, this is 
> true" properties to verify other properties it *can* verify.

Oh, I forgot "thirdly".

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.

BTW, simple but run-time expensive conditions are more likely to be proven 
by the tool (at least for SPARK) than equivalent faster algorithms. E.g., 
I'd prefer

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

over

   pre => (for I in 2 .. SQRT(N) => (N mod I /=0))

even though the second would be much faster if performed at run time.

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