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

[Tim Rowe <spamtrap@tgrowe.plus.net>]

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?