Newbie question: SPARK verification condition on member of private record

Newbie question: SPARK verification condition on member of private record

[Tim Rowe]

Ok, I've been busily reading all of the spark documentation, and there's 
just one thing I'm stuck on at the moment.

I have:
    subtype Array_Index is Integer range 1..5000;
    type Foo is private;
    function Get_Order(This: in Foo) return Array_Index;
    -- other specifications

and in the private part I have
    type Foo is record
       Highest_Valid_Index: Array_Index;
       -- other definitions
    end record;

The body of Get_Order is simply
    function Get_Order(This: in Foo) return Array_Index is
    begin
       return This.Highest_Valid_Index;
    end Get_Order;

My problem is that I'm getting a proof obligation
H1:    get_order(this) < 5000 .
C1:    fld_highest_valid_index(this) <= 4999 .
If I'm reading that correctly then it's clearly true, but I would like 
to be able to annotate the code so that Examiner knows that 
get_order(this) = fld_highest_valid_index(this). My instinct is to 
annotate Get_Order with
    --# return This.Highest_Valid_Index;
but that's not allowed (" Semantic Error    :  9: Selected components 
are not allowed for This.")

So how should I annotate or restructure the code to make the 
relationship between Get_Order(This) and This.Highest_Valid_Index?

Thanks,

Tim Rowe

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

[JP Thornley]

In article <jsudnfEigqAgX07UnZ2dnUVZ8ridnZ2d@posted.plusnet>, Tim Rowe 
<spamtrap@tgrowe.plus.net> writes
>Ok, I've been busily reading all of the spark documentation, and 
>there's just one thing I'm stuck on at the moment.
>
>I have:
>   subtype Array_Index is Integer range 1..5000;
>   type Foo is private;
>   function Get_Order(This: in Foo) return Array_Index;
>   -- other specifications
>
>and in the private part I have
>   type Foo is record
>      Highest_Valid_Index: Array_Index;
>      -- other definitions
>   end record;
>
>The body of Get_Order is simply
>   function Get_Order(This: in Foo) return Array_Index is
>   begin
>      return This.Highest_Valid_Index;
>   end Get_Order;
>
>My problem is that I'm getting a proof obligation
>H1:    get_order(this) < 5000 .
>C1:    fld_highest_valid_index(this) <= 4999 .
>If I'm reading that correctly then it's clearly true, but I would like 
>to be able to annotate the code so that Examiner knows that 
>get_order(this) = fld_highest_valid_index(this). My instinct is to 
>annotate Get_Order with
>   --# return This.Highest_Valid_Index;
>but that's not allowed (" Semantic Error    :  9: Selected components 
>are not allowed for This.")
>
>So how should I annotate or restructure the code to make the 
>relationship between Get_Order(This) and This.Highest_Valid_Index?

The easiest way to deal with this is to create a user rule to replace 
get_order(X) with fld_highest_valid_index(X):

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.

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

The name of the rule file must be X.rlu where X is either the name of 
the operation that the VC is generated by or the name of the package 
that the operation is in.  The file must appear in the folder containing 
the vcg etc. files of the operation.
(When the Simplifier starts on a file op_name.vcg in folder pack_name it 
looks for user rule files called op_name.rlu and pack_name.rlu, so 
op_name.rlu should have rules that are specific to the operation and 
pack_name.rlu should have rules that are applicable throughout the 
package.)

If this doesn't work then you may need a more specific rule, such as
a_name(2): fld_highest_valid_index(X) <= 4999 may_be_deduced_from
            [ get_order(X) < 5000 ].
with the same justification.

Hope this helps - for more info read section 7 of the Simplifier User 
Manual which is all about user rules.

Cheers,

Phil
-- 
JP Thornley

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

[Tim Rowe]

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?

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

[JP Thornley]

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

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

[Tim Rowe]

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

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

[JP Thornley]

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

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

[roderick.chapman]

I concur with Phil.  It's almost _always_ better to write
aggregate expressions and use the array/record update notation
in postconditions than using field-by-field assignments
and equalities.

e.g.

Do write

 A := T'(X, Y, Z);

Don't write

 A.F1 := X;
 A.F2 := Y;
 A.F3 := Z;

Also...for just

 A.F1 := X;

the correct post-condition would be

 --# post A = A~[F1 => X];

which defines the final value of the whole object, rather than

 --# post A.F1 = X;

which defines the final value of A.F1 but leaves the other
2 fields unspecified.  Further explanation of all this in the
"Generation of VCs" manual.

 - Rod Chapman, SPARK Team

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

[Tim Rowe]

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.

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

But less entertaining for bystanders.

In fact, in this case I wouldn't have noticed anything wrong. When 
specifying that all original members of the array would be unchanged, I 
accidentally appended a tilde to "This" on /both/ sides of the identity, 
so it was trivially true. It would probably have vanished in the 
simplifier, and I wouldn't have known anything was wrong. Thank goodness 
for peer review and testing in the Real World! (And the low likelihood 
of a typing error in the annotation aligning with a corresponding error 
in code).

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

[Tim Rowe]

roderick.chapman@googlemail.com wrote:
> I concur with Phil.  It's almost _always_ better to write
> aggregate expressions and use the array/record update notation
> in postconditions than using field-by-field assignments
> and equalities.
> 
> e.g.
> 
> Do write
> 
>  A := T'(X, Y, Z);
> 
> Don't write
> 
>  A.F1 := X;
>  A.F2 := Y;
>  A.F3 := Z;

Except in this case that makes the VCs a lot more complicated. You 
covered that by saying /almost/ always, of course.

> Also...for just
> 
>  A.F1 := X;
> 
> the correct post-condition would be
> 
>  --# post A = A~[F1 => X];

Except that in this case the type of A is private, so I can't (as far as 
I can tell) access its fields from a postcondition.

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

[JP Thornley]

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

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

[Tim Rowe]

JP Thornley wrote:

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


Correct on both counts -- it greatly simplifies the VCs (each one now 
reads quite naturally) and it is completely non-intuitive :-)

I'll go and scratch my head for a while to figure uoit how this works -- 
which I think mainly comes down to figuring out why the fields of the 
private type are visible for the postcondition of the local operation 
when they weren't visible for annotations of the enclosing operation.

Thanks for your help, anyway -- clearly I still have a long way to go, 
but I feel that with your (and Rod's) help I'm making good progress.