Re: SPARK prooving an array of Positives.

[Brad Moore <bmoore.ada@gmail.com>]

I got this to prove in SPARK by making a couple of modifications.

The first thing I noticed is that post conditions of First and Last are trying to show that the result is not larger than the Positive type maximum value.

I find it is a good idea to simplify the code, as it usually helps the proofing effort. If the result type of First and Last is of subtype Positive, then there should be no need to prove anything, since Positive'Last = Max.

So I changed the result type to Positive. 
After doing that, the prover was happy about the First and Last functions, but was complaining about the case statement when Item'Length is 2, 

   i.e.  I had written, 
       when 2 =>  return Unsigned_64(First * Last);

SPARK wanted me to prove that this multiplication cannot cause a numeric overflow. This is a problem now because First and Last are of type Positive, and the result of multiplying the worst case positive values, Positive'Last*Positive'Last would overflow, so I needed to convert the results of First and Last to 64 bit unsigned values before doing the multiplication.
The SPARK prover is now happy because it can tell that the multiplying the two 31 bit values after converting to 64 bits will not overflow a 64 bit value.

I hope you don't mind, but I took the liberty of applying the GNAT style guidelines to the code, after turning on most style and warnings, and addressing those. I also made a couple other changes that I thought might have helped the prover, but I doubt was necessary, but something to keep in mind, and seemed to be improvements, but I don't think any of these changes likely helped the SPARK prover.

For example, rather than use subtype Positive, and Interfaces.Unsigned_64, I think it helped to define more specific types to fit the code problem.
That is, instead of Positive, I defined type Axis_Value. This is a type definition, rather than a subtype definition. This might be helpful for SPARK since the type definition is a compile-time definition, whereas subtypes typically involve dynamic checking at run time to ensure that the range constraints are being applied. I think generally SPARK would have an easier time analyzing code if it can rely on compile time constraints. 

I think also having the Axis_Value type declared makes it clearer in the code the number of bits associated with the type, rather than Positive, which can be more target-dependent.

Also, instead of using Interfaces.Unsigned_64, I defined the type Result_Value, which seems to help clarify to the reader, and eliminate the need for clients to with an extra package.

package FITS with SPARK_Mode is

   type Result_Value is mod 2 ** 64;
   for Result_Value'Size use 64;

   type Axis_Value is range 1 .. +(2 **31 - 1);
   for Axis_Value'Size use 32;
   
   type Axis_Count is range 0 .. 999   with Size => 10;

   type Axis_Dimensions is array (Axis_Count range <>) of Axis_Value
     with Default_Component_Value => 1;

   subtype Primary_Data_Array is Axis_Dimensions (1 .. 999);
   subtype Random_Groups_Data is Axis_Dimensions (1 .. 998);

   function EF (Item : FITS.Axis_Dimensions) return Result_Value;

end FITS;

package body FITS with SPARK_Mode is

   function EF (Item : FITS.Axis_Dimensions) return Result_Value
   is
      function First return Axis_Value is (Item (Item'First))
        with Inline,
             Pre => Item'Length > 0;

      function Last return Axis_Value is (Item (Item'Last))
        with Inline,
             Pre => Item'Length > 0;

   begin -- EF

      case Item'Length is
         when 0      => return 1;
         when 1      => return Result_Value (First);
         when 2      => return Result_Value (First) * Result_Value (Last);

         when others =>
            declare
               Middle : constant Axis_Count := Item'Length / 2 + Item'First;
               subtype Head is Axis_Count range Item'First .. Middle;
               subtype Tail is Axis_Count range
                 Axis_Count'Succ (Middle) .. Item'Last;
            begin
               return EF (Item (Head)) * EF (Item (Tail));
            end;
      end case;

   end EF;

end FITS;

Brad