Re: SPARK : third example for Roesetta - reviewers welcome

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sun, 15 Aug 2010 20:42:27 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
>
>>           Position := Index_Type'First;
>>           -- Default value (required to not a have a data flow error).
> It's bad practice to put in an unnecessary assignment to get rid of a
> flow error.  It is much better to structure the code to avoid the flow
> error.  (They can hide genuine flow errors.)  In this case you can get
> rid of this one by not defining the variable Middle and using Position
> instead - since Position is simply assigned to Middle once a value is
> found.
I see the point. I though about this one first and then changed my mind,  
may be for two bad reasons (will have to be checked) : first may be I did  
useless "optimization" (do not know how good compilers handle this), and  
then, I though this may be better if ever the context may have some kind  
of tasking. About the latter, I will have to check if weither or not an  
out value is supposed to be updated only when the method exit or is  
possibly updated outside while the method is running.

>>        for Source_Index in
>>           Binary_Searchs.Index_Type range Source'Range
>>        loop
>>           --# assert True;
>>           -- No need for an assertion on anything.
> If you don't need an assertion then don't put one in.  If you want to
> get rid of the warning about the default assertion then just put
> 'default_loop_assertions' into your warning file.
I was wondering about reader which may try the example as-is. As was  
"afraid" to think someone may try it and see that "unexpected" message  
 from the Examiner. Or may be there is a place some kind of more  
useful-looking assertion here instead of a dummy one ?

OTH, while I thinking about your comment, I cannot avoid this though:  
after all, if a loop assertion is really missing, this inevitably ends up  
into undischarged Validation Conditions. So in some sense, this warning is  
useless, because 1) when it is meaningful, it is redundant with later  
reports of undischarged VC 2) if this does not ends into undischarged VC,  
this is not meaningful. So, this is either not meaningful either  
redundant. May be this is disabled by default in the Examiner's builtin  
options ?

... I still wonder about readers who may get this warning without this.  
But for Real Use, I agree with you, the idea of disabling this warning is  
indeed good.


>>           SPARK_IO.Put_Integer
>>             (File  => SPARK_IO.Standard_Output,
>>              Item  => Source_Index,
> This line just prints the index - should be Item =>
> Source(Source_Index),
Don't mind for this one Phil, this was a transient modification which  
occurs at the same time I was posting this here (I did both thing at the  
time and did not notice I was posting an error). The one at Rosetta do  
Source (Source_Index); it was corrected in the afternoon (local time, lol).

>>        case Success is
>>           when True =>
> A case statement for a Boolean is just a waste of typing.  Also I
> don't think 'Success' is a good name for this variable as the program
> always 'succeeds'.  'Found' would be a more descriptive name and is
> more clearly a Boolean term.
Mmmh, your informal argument makes me think this may be matter of taste  
this one, both for case and name. However, will think about it. Well, you  
may be right for Success vs Found ; will change it ; except for Case  
Statement which I do not wish to change for the time. I have reasons for  
that, but don't want to argue about it here (to not obfuscate the topic,  
... will just say, to keep it simple, I don't enjoy the “else” branches of  
"if-then" constructs... I call it “the mute branch”).

>> * The test part, that is Run_Search and body of Program takes up to  
>> half of all of the source. Should I remove it or not ?
> I don't think so - it seems to be a good idea to provide runable
> programs where appropriate.
OK. As there was a doubt in my mind about it, I added a comment suggesting  
to focus only on the relevant part. So I may remove it. Will have this in  
mind for future example.

>> * In the loop inside of Search there are Check annotations which was  
>> not strictly needed but which I still left for more expressiveness. Is  
>> that OK ? Not too much ?
> I prefer user rules to large numbers of check annotations, but YMMV.
I don't want to introduce user rules at Rosetta, because don't think this  
is the place for such none-straight-way things.

About Real Use, this is another topic.

>> * To keep it simple so far, I have dropped a precondition which I  
>> initially started with and which was requiring the array to be sorted.  
>> This only impact semantic, not runtime check, as any way, the subrange  
>> width always decrease, so that the loop always terminates. Should I or  
>> should I not get it back ?
> See my version below (which requires this precondition).
OK. Will see right after (I reply as I read)

>> * I also though about an indirect way to prove the loop always  
>> terminates
>> (although this is not a feature supported by SPARK, there are indirect
>> ways to achieve this). I though this would look like too much obfuscated
>> if I add it. Do you agree this would be a bad idea or on the opposite do
>> you feel this would be an opportunity to show something interesting ?
> No - keep is as simple as possible (but not simpler...).

>> * If Success (as return by Search) is False then Position is not  
>> guaranteed to mean anything, simply because in such a circumstance, no  
>> postcondition about it applies. I did this way, because I do not know a  
>> way to explicitly state “This is undefined”. Do you know a better way  
>> to express it ? (I could have used a discriminated type for that  
>> purpose, but SPARK disallow this... as you know).
> Strengthening the postcondition is a good idea, and one I've followed
> up on, see below...


>> Oops, as last question: I did not understood why, once a time, POGS  
>> returns me two reports for the same single Run_Test procedure, one  
>> which was saying OK and one which
> I think you might get this if you get a syntax error from the Examiner
> when generating VCs.
And this could end into two SIV files in the same folder for the same  
procedure ?


> I decided that it would more interesting to strengthen the post-
> condition to say that 'not Success' means that no element in Source is
> equal to Item.
May be I see. This suggest the most typical or expected result is Found,  
instead of not Found, and so you are focusing on the consequence of not  
Found, which are more likely to need care.

> Since this can't be proved without using user rules, I got rid of the
> checks for the 'div' calculations and added two rules for these as
> well.
>
> I had to introduce a precondition that the Source array is ordered,
> otherwise the rules wouldn't work.
> (This leaves an unproven VC in Run_Search, but I don't think this is a
> big issue.)
>
> This is getting a bit too big to post, so the code and user rules are
> in http://www.sparksure.com/resources/Rosetta_Binary_Search.txt
OK. The cool stuff to read is there :)


I enjoy your contribution, with the one of Jeffrey too. I was pleased.

Well, well, now time to read your version. "See" you soon.



-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.