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

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

In article <JKKdnWLcDdxDNUnUnZ2dnUVZ8sCWnZ2d@posted.plusnet>, Tim Rowe 
<spamtrap@tgrowe.plus.net> writes
>That's giving me conclusions to prove like:
>H1:    get_order(this) < 5000 .
>H2:    1 - get_probability(this) >= event_conjunctions__get_probability(
>          conjunction) .
>H3:    fld_highest_valid_index(this) >= 1 .
>H4:    fld_highest_valid_index(this) <= 4999 .
>       ->
>C1:    get_order(upf_probability(upf_events(upf_highest_valid_index(this,
>          fld_highest_valid_index(this) + 1), update(fld_events(this), [
>          fld_highest_valid_index(this) + 1], conjunction)), 
>fld_probability(
>          this) + event_conjunctions__get_probability(conjunction))) =
>          get_order(this) + 1 .
>
>That's one of the easier ones. The point is that upf_probability, 
>upf_events and update can't affect the result of get_order. Knowing 
>that I can reduce the espression to
>       get_order(
>          upf_highest_valid_index
>          (
>             this, fld_highest_valid_index(this) + 1
>          )
>       ) = get_order(this) + 1
>
>which I can prove easily enough, but the process seems error prone (as 
>I say, this is one of the simpler ones). If I /could/ give the tools 
>some hints to reduce it it would be a big help. Maybe I /should/ make 
>the record public!
Well, it all depends on how much rigour you need.

For a fully rigorous proof you have to use the Proof Checker on the 
generated VC as this will only let you eliminate upf_/update's if it is 
valid to do so.

For a less rigorous proof you create one or more user rules that 
eliminate the upf_/updates and, if you feel the need, justify the rule 
by creating and proving the equivalent VC in the Proof Checker.

The usual recommendation for updating records is to assign an aggregate 
rather than individual components (this gets rid of all the 
upf_/update's), but the need to update an element of the array makes it 
more awkward in this case. If the record had any more components I would 
recommend separating out the array and its index to their own record 
type, but that is probably overkill here.

>
>
>If nothing else, I found an error in the postcondition by explaining 
>this ;-)

That's a lot easier than the usual way (banging head against desk until 
you eventually realise that it's not a problem with the tools).

Phil

-- 
JP Thornley