On Mon, 11 May 2015, Randy Brukardt wrote:

> <Stefan.Lucks@uni-weimar.de> wrote in message
> news:alpine.DEB.2.11.1505111113020.12062@debian...

>> 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. :-)

Firstly, have to write that. Somehow! Otherwise, my documentation would be 
seriously incomplete.

Either I write it as a second-class precondition in the form of a comment, 
or as a fist-class precondition using the "pre" attribute, or something 
similar ("unchecked_pre" or whatever). I'd prefer the second, because the 
compiler will tell me if my precondition is syntactically correct.

Yes, I claim that Ada12-style pre- and postconditions are helpful, even if 
they are neither verified statically nor verified at run time.

I have seen too many informal specifications that didn't fit. As an 
example, consider

   function Divide (Dividend, Divisor: Num) return Num;
   -- Precondition: Y /= To_Num(0).

This example is simple and harmless. One can easily guess that at some 
point of time, the parameter "Y" has been renamed to "Divisor", but the 
comment has not been updated. Similar cases can be a lot more complicated. 
Having a precondition parsed by the compiler is a big win, even if the 
compiler does nothing beyond parsing with the precondition.

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

> I don't begin to believe that all program properties can be proved.

Ah! Some of your previous posts left me with the impression that you where 
proposing an "either prove everything, or don't prove anything" approach.

>> In practice, people usually call the Miller_Rabin primality test:
>>
>>    function MR_Is_Prime(N: Num; Repetitions: Natural := 500)
>>             return Boolean with
>>      post => Miller_Rabin_Prime'Result = Is_Prime(N);
>>
>> As a specification, the postcondition is useful.
>
> I disagree, actually. I think any useful postcondition has to be reasonably
> executable. Else there is no difference from a comment,

See above.

> and you would be better served using a comment as won't throw out all of 
> the easy checks with this silly one.

Firstly, see my above writing on comments versus compiler-parsed 
specifications.

Secondly, this property may actually be relevant to statically verify 
other program properties, under the assumption that the "believe me" claim 
is true.

> No, by my logic, *writing* a test that you can't actually execute is bad, as
> it tells no one anything useful.

I think, this is the core point of our disagreement -- or your 
misunderstanding, as I would put it. ;-)

You can check a precondition or a postcondition or an invariant for 
testing purposes. But neither *is* a test, and either can have other 
purposes than just testing.

> I don't think anyone would ever want a system that *required* proving
> everything. The important thing IMHO is that you  can find out what wasn't
> proven so you can determine whether to fix it (via additional
> specifications) or whether to ignore it (the obvious case being that the
> unproven case is on a non-executable path).

We are in violent agreement here.

But this is precisely the reason why I am trying to advertise a 
fine-grained way to separate between things proven at compile time or 
checked at run time (and maybe checked at testing versus also checked in 
production code) from things claimed. I don't care much about the syntax, 
some "unchecked_pre", "unchecked_post" attributes would be perfectly fine.

> I want to bring this tool to people that would not go out of their way to
> use it. (I.e., me. :-) That means it has to be in the compiler so that they
> get the benefits automatically, because there is no way I'm going out and
> buying (plus learning) a separate tool to do those things. I suspect that
> many (perhaps most) programmers are like me. Like everyone, I want it all,
> for free, right now. :-) Only Ada comes close, and I just want to make it
> closer.

Violent agreement, again!

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