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

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

In article <y7ednbO7TLaJzEjUnZ2dnUVZ8sSdnZ2d@posted.plusnet>, Tim Rowe
<spamtrap@tgrowe.plus.net> writes
>JP Thornley wrote:
>
>> 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.
>
>Yes, an aggregate assignment followed by the update of the array makes
>for a much worse set of things to prove.

Although you get some fearsome looking expressions sometimes, it is
often the case that a rule that proves a conclusion is much simpler.
If you want to send me some sparkable code to play with then use the
email address on www.sparksure.com.

An alternative that sometimes works when updating arrays is to move the
update into a local operation (it's completely non-intuitive code but
often creates easier proofs).

If your code looks something like:
      This.Highest_Valid_Index => This.Highest_Valid_Index + 1;
      This.Events(This.Highest_Valid_Index) := Conjunction;

then add the following as a local procedure and call it in place of the
second statement above (it shouldn't cost anything in execution time as
the compiler should be able to inline it)

      procedure Set_Element
      --# global in out This;
      --#        in     Conjunction;
      --# derives This from *, Conjunction;
      --# post This.Probability = This~.Probability and
      --#      This.Highest_Valid_Index = This~.Highest_Valid_Index and
      --#      This.Events = This~.Events[New_Index => Conjunction];
      is
      begin
         This.Events(This.Highest_Valid_Index) := Conjunction;
      end Set_Element;
      pragma Inline(Set_Element);

you may find that any VCs left by the Simplifier are now easier to read.

Phil

-- 
JP Thornley