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

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

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