Spark-Ada postcondition for array total

Question

How does one write a Spark postcondition for a function that sums the elements of an array? (Spark 2014, but if someone shows me how to do it for an earlier Spark I should be able to adapt it.)

So if I have:

type Positive_Array is array (Positive range <>) of Positive;

function Array_Total(The_Array: Positive_Array) return Positive
with
  Post => Array_Total'Return = -- What goes here?
is
  -- and so on

I don't need to worry about overflow in my particular case (I know what the total was at initialisation, and it can only monotonically decrease).

Presumably I'll need a loop variant in the implementation, to help the prover, but that should be straightforward variation of the postcondition, so I'm not worried about that yet.

Answer 1

This is an old, yet interesting question. Here's a late answer, just for completeness and future reference.

The main "trick" on how to solve these kind of problems was given in the blog post Taking on a Challenge in SPARK posted on AdaCore's website.

Opposed to what was already suggested by some of the answer's, you cannot use a recursive function to prove the summation. Instead, you need a ghost function as shown in the example below. The method can be extended in order to proof similar "list folding" operations such as (conditional) counting.

The example below can be proven with GNAT CE 2019 with proof level 1.

Update July 2020

Small improvement in postcondition of Sum_Acc. See also this related answer for another example.

sum.ads

package Sum with SPARK_Mode is

   --  The ranges of the list's index and element discrete types must be
   --  limited in order to prevent overflow during summation, i.e.:
   --
   --     Nat'Last * Int'First >= Integer'First   and
   --     Nat'Last * Int'Last  <= Integer'Last
   --
   --  In this case +/-1000 * +/-1000 = +/-1_000_000 which is well within the 
   --  range of the Ada Integer type on typical platforms.
   
   subtype Int is Integer range -1000 .. 1000;
   subtype Nat is Integer range     0 .. 1000;
   
   type List is array (Nat range <>) of Int;
   
   
   --  The function "Sum_Acc" below is Ghost code to help the prover proof the
   --  postcondition (result) of the "Sum" function. It computes a list of
   --  partial sums. For example:
   --
   --     Input   :  [ 1  2  3  4  5  6 ]
   --     Output  :  [ 1  3  6 10 15 21 ]
   --
   --  Note that the lengths of lists are the same, the first elements are
   --  identical and the last element of the output (here: "21"), is the
   --  result of the actual function under consideration, "Sum".
   --
   --  REMARK: In this case, the input of "Sum_Acc" and "Sum" is limited
   --          to non-empty lists for convenience.
   
   type Partial_Sums is array (Nat range <>) of Integer;
   
   function Sum_Acc (L : List) return Partial_Sums with 
     Ghost,
     Pre  =>  (L'Length > 0),
     Post =>  (Sum_Acc'Result'Length = L'Length) 
     and then (Sum_Acc'Result'First = L'First) 
     and then (for all I in L'First .. L'Last =>
                 Sum_Acc'Result (I) in 
                   (I - L'First + 1) * Int'First .. 
                   (I - L'First + 1) * Int'Last)
     and then (Sum_Acc'Result (L'First) = L (L'First))
     and then (for all I in L'First + 1 .. L'Last =>
                 Sum_Acc'Result (I) = Sum_Acc'Result (I - 1) + L (I));
   
   
   function Sum (L : List) return Integer with
     Pre  => L'Length > 0,
     Post => Sum'Result = Sum_Acc (L) (L'Last);

end Sum;

sum.adb

package body Sum with SPARK_Mode is

   -------------
   -- Sum_Acc --
   -------------
            
   function Sum_Acc (L : List) return Partial_Sums is
      PS : Partial_Sums (L'Range) := (others => 0);
   begin
      
      PS (L'First) := L (L'First);
      
      for Index in L'First + 1 .. L'Last loop
      
         --  Head equal.
         pragma Loop_Invariant
           (PS (L'First) = L (L'First));
         
         --  Tail equal.
         pragma Loop_Invariant
           (for all I in L'First + 1 .. Index - 1 =>
              PS (I) = PS (I - 1) + L (I)); 
         
         --  NOTE: The loop invariant below holds only when the range of "Int" 
         --        is symmetric, i.e -Int'First = Int'Last. If not, then this
         --        loop invariant may have to be adjusted.
         
         --  Result within bounds.
         pragma Loop_Invariant 
           (for all I in L'First .. Index - 1 =>
              PS (I) in (I - L'First + 1) * Int'First ..
                        (I - L'First + 1) * Int'Last);
               
         PS (Index) := PS (Index - 1) + L (Index);
      
      end loop;
      
      return PS;
      
   end Sum_Acc;

   ---------
   -- Sum --
   ---------
   
   function Sum (L : List) return Integer is
      Result : Integer := L (L'First);
   begin
      
      for I in L'First + 1 .. L'Last loop
         
         pragma Loop_Invariant
           (Result = Sum_Acc (L) (I - 1));
         
         Result := Result + L (I);
        
      end loop;
      
      return Result;
      
   end Sum;

end Sum;

Answer 2

One way to write the postcondition could be as a recursive function. That would avoid the problem of the implementation and specification being exactly the same.