Пост-условие Spark-Ada для итогового массива

Question

Как написать постусловие Spark для функции, которая суммирует элементы массива? (Spark 2014, но если кто-то покажет мне, как это сделать для более ранней версии Spark, я смогу адаптировать ее.)

Так что если у меня есть:

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

Мне не нужно беспокоиться о переполнении в моем конкретном случае (я знаю, какова была общая сумма при инициализации, и она может только монотонно уменьшаться).

Предположительно, мне понадобится вариант цикла в реализации, чтобы помочь пруверу, но это должно быть простым изменением постусловия, так что я пока не беспокоюсь об этом.

Answer 1

Это старый, но интересный вопрос. Вот поздний ответ для полноты и справки в будущем.

Главный "трюк" о том, как решить такого рода проблемы, был описан в сообщении блога " Принимая вызов в SPARK", размещенном на веб-сайте AdaCore.

В отличие от того, что уже было предложено некоторыми ответами, вы не можете использовать рекурсивную функцию для доказательства суммирования. Вместо этого вам понадобится функция-призрак, как показано в примере ниже. Этот метод может быть расширен для подтверждения аналогичных операций "сворачивания списка", таких как (условный) подсчет.

Приведенный ниже пример можно проверить с помощью GNAT CE 2019 с уровнем доказательности 1.

Обновление июль 2020 г.

Небольшое улучшение постусловия Sum_Acc. См. Также этот связанный ответ для другого примера.

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

Одним из способов написания постусловия может быть рекурсивная функция. Это позволило бы избежать проблемы, связанной с реализацией и спецификацией, которые были бы точно такими же.