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

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

JP Thornley wrote:

> 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).

The other proof obligations I'm getting /are/ for partial correctness. 
An operation that changes a lot of fields in the private record has a 
postcondition describing what the effect should be on each field. But I 
can only describe that effect in terms of the Get_xxx functions. That 
means that, for instance, the postcondition on Get_Order is padded with 
a lot of stuff about the updating of fields that have no effect on 
Get_Order.

> 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.

Unfortunately, the fields of the private type are related, so they all 
change together for consistency.

Maybe I should get more specific. As a tutorial exercise, I'm looking at 
what an existing program for transforming the format of a fault tree 
report file would look like in SPARK -- not with the intention of using 
it, but so that I understand SPARK better.

So the private type in question is:
    type Cut_Set is record
       Probability         : Probability_Type;
       Events              : Event_Array_Type;
       Highest_Valid_Index : Array_Index;
    end record;
and I add an event to the cutset with
    procedure Add
      (This        : in out Cut_Set;
       Conjunction : in Event_Conjunctions.Event_Conjunction);
    --# derives This from *,
    --#                   Conjunction;
    --# pre Get_Order(This) < Array_Index'Last and
    --#     1.0 - Get_Probability(This) >=
    --#		Event_Conjunctions.Get_Probability(Conjunction);
    --#
    --# post (Get_Order(This) = Get_Order(This~) + 1) and
    --#      (for all I in Array_Index range 
Array_Index'First..Get_Order(This~)
    --#		=> (Get_Conjunction(This, I) = Get_Conjunction(This~, I))) and
    --#      Get_Conjunction(This, Get_Order(This)) = Conjunction and
    --#      Get_Probability(This) =
    --#		Get_Probability(This~) +
    --#		Event_Conjunctions.Get_Probability(Conjunction);
(As previously mentioned, Get_Order returns Highest_Valid_Index, and 
yes, I am aware of the issues with testing for equality on floats and 
that I have a hidden assumption that Array_Index'First = 1).

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!


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