Re: Newbie question: SPARK verification condition on member of private record

[JP Thornley <jpt@diphi.demon.co.uk>]

In article <et6dnUO6O_dLYE7UnZ2dnUVZ8o-dnZ2d@posted.plusnet>, Tim Rowe 
<spamtrap@tgrowe.plus.net> writes
>JP Thornley wrote:
>
>> The rule should look like:
>> a_name(1): get_order(X) may_be_replaced_by fld_highest_valid_index(X).
>> where 'a_name' can be any name you like. X will be treated as a 
>>wildcard  that matches to anything in the VC.
>
>That works nicely, thanks. Although...
>
>> The justification for the rule is the code of the function Get_Order. 
>>It  really would be nice to have a return annotation on the function 
>>but, as  you have found, this isn't possible with private types.
>> [Actually it is possible, but very longwinded and involves the 
>>additional definition of a proof function, so it isn't usually 
>>considered worthwhile for such simple code.]
>
>... I'll probably want to get around to that approach eventually. In 
>fact, sooner rather than later I think. Otherwise for some of the other 
>proof obligations it looks as if I'm going to need a lot of user rules 
>to tell the simplifier that various operations don't affect the results 
>of Get_Order. I had thought of proof functions but couldn't see how not 
>to move the same problem into the proof function.
>
>How long-winded is long-winded?

Yes, information hiding is a great idea for structuring software but 
becomes something of a pain when it comes to proof - and you end up 
exposing various aspects of the hidden code.

However I would never recommend degrading the software structure to make 
proof easier - at least for proof of absence of run-time error (proof of 
partial correctness may be a different matter).

In this case you may need to add postconditions on various operations 
that update objects of the private type, to say that the result of 
Get_Order is unchanged by the operation, but this is probably better 
than the alternative - which is make the type visible.

For proof of absence of run-time error it is normal practice only to add 
proof annotations in response to unprovable VCs, so you may find that 
only a few operations need a postcondition for unchanged Get_Order.

On the function return annotation - you cannot avoid the use of a user 
rule here as function return annotations have no effect on the 
hypotheses of VCs generated subsequent to the function call.  This is 
the big difference between function return annotations and procedure 
postconditions. The only thing that function return annotations do is 
provide the supporting argument for one or more rules about the result 
of the function (and which can be applied to the VCs subsequent to the 
function call as that call will appear in the VC).

The 'long-winded justification' simply provides a supporting argument 
that is more rigorous than 'go and look at the code'.

Phil

-- 
JP Thornley