如何使用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 ; 

我想用Assert和loop_invariants编写PolyPack包的主体，这样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 ;

格纳特证明：

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溢出或下溢？

我也很好奇为什么要忽略Vector中的最后一个值。您是否正在尝试反向遍历数组？如果是这样，只需使用以下for循环语法：

for I in reverse A'Range loop