Re: SPARK Question

[Phil Thornley <phil.jpthornley@gmail.com>]

In article <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com>, 
enzmann.m@googlemail.com says...

[snip]

> The vector can now hold a maximum of "Number_Of_Elements" Values, 
although the actually used length will in most cases be smaller. This 
"true" length is shown by the component "Length" in the record.
> 
> Reading a single element of the vector now needs a function
> 
> >   function Get_Value
> >     (The_Vector : in Basic_Vector;
> >      At_Position : in Positive)
> >      return Basis_Type;
> >   --# PRE At_Position in Array_Range;
> 
> which clearly will not work if "At_Position" is larger than "Number_Of_Elements". Furthermore it will however not give a useful result, if "At_Position" is larger than "The_Vector.Length".
> 
> How can I express this in a pre-condition? I can write a function
> 
> >   function Vector_Length (The_Vector : in Basic_Vector) return Positive;
> 
> and use this in the pre-condition. This leaves however a couple of questions open, so I'd prefer to do this in a different way.
> 
> As far as I understand, a proof-function 
> 
> >   --# function Vec_Length (The_Vector : in Basic_Vector) return Positive;
> 
> 
> could do the trick in the specification and a more elaborate version of the
> pre-condition will then be used in the body. I have however no idea, how the
> two are linked and how I can express the relationship in the rules file.

Assuming you are using the latest version of SPARK, the simplest way to 
do this is to also include the proof function Vec_Length in the body, 
and give it a return annotation. So in the spec put:

   --# function Vec_Length (The_Vector : in Basic_Vector)
   --#   return Positive;

   function Get_Value
     (The_Vector : in Basic_Vector;
      At_Position : in Positive)
      return Basis_Type;
   --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector);

and in the body put:

   --# function Vec_Length (The_Vector : in Basic_Vector)
   --#   return Positive;
   --# return The_Vector.Length;

With the other code as you have it in your post, this leaves one 
unprovable VC for Get_Value, as the value of Length in the record is 
declared as Natural.  If  this is changed to Array_Range it makes the VC 
provable, and proved by the Simplifier. (But this then means that you 
cannot have an empty vector - which can be fixed by declaring another 
subtype for Length that includes 0).

You need to be aware that by doing it this way rather than having a 
coded function for Vec_Length (which you say you don't want to do) you 
are making a claim for Vec_Length that cannot be validated by the proof 
tools.  (See section 3.3 of the document "Calling functions in SPARK 
proof contexts").

Cheers,

Phil