时间戳

首页 > 解决方案 > 如何使用 Assert 和 loop_invariants

ada - 如何使用 Assert 和 loop_invariants

问题描述

规格：

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 的正确性。

我写了我的函数 Horner 但我不知道如何在这个程序中放置断言和 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 删除溢出检查

标签： adaformal-verificationspark-adaspark-2014

解决方案

分析是正确的。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

推荐阅读