Как использовать Assert и loop_invariants

Question

Спецификация:

package PolyPack with SPARK_Mode is 
type Vector is array (Natural range <>) of Integer;
function RuleHorner (X: Integer; A : Vector) return Integer
with
Pre => A'Length > 0 and A'Last < Integer'Last;
end PolyPack ; 

Я хочу написать тело пакета PolyPack с Assert и loop_invariants, чтобы программа gnatprove могла доказать правильность моей функции RuleHorner.

Я пишу свою функцию Хорнер, но я не знаю, как поместить утверждения и loop_invariants в эту программу, чтобы доказать ее суть:

with Ada.Integer_Text_IO;
package body PolyPack with SPARK_Mode is

   function RuleHorner (X: Integer; A : Vector) return Integer is
      Y : Integer := 0;
      begin       
      for I in 0 .. A'Length - 1 loop
         Y := (Y*X) + A(A'Last - I);
      end loop;
      return Y;
      end RuleHorner ;
end PolyPack ;

gnatprove:

overflow check might fail (e.g. when X = 2 and Y = -2)
overflow check might fail

проверка переполнения для строки Y:= (Y*X) + A(A'Last - I);

Может кто-нибудь помочь мне, как удалить проверку переполнения с loop_invariants

Answer 1

Анализ правильный. Тип элемента для типа Vector - Integer. Когда X = 2, Y = -2 и A(A'Last - I) меньше, чем Integer'First + 4, произойдет недостаточное заполнение. Как вы думаете, это должно быть обработано в вашей программе? Инварианты цикла не будут работать здесь, потому что вы не можете доказать, что переполнение или переполнение не может произойти. Есть ли способ, которым вы можете спроектировать свои типы и / или подтипы, используемые в Vector и для переменных X и Y, чтобы предотвратить переполнение или недостаточное переполнение Y?

Мне также любопытно, почему вы хотите игнорировать последнее значение в вашем векторе. Вы пытаетесь пройти через массив в обратном порядке? Если это так, просто используйте следующее для синтаксиса цикла:

for I in reverse A'Range loop