如何使用 Assert 和 loop_invariants答案

【问题标题】：How to use Assert and loop_invariants如何使用 Assert 和 loop_invariants
【发布时间】：2019-03-09 00:33:17
【问题描述】：

规格：

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 删除溢出检查

【问题讨论】：

尝试运行Rulehorner (1, (Integer'Last, Integer'Last));它给出了一个Constraint_Error。
@Simon Wright 你知道如何用 spark 改进规范和 body horner_rule 来证明所有断言吗？
我的意思是你不能证明从目前的情况来看没有异常，因为这个函数将引发异常的输入！它是你的函数，你可以通过说明它应该做什么来帮助自己，最好以更好的前置条件和后置条件的形式。英语是一个开始；我不知道。

标签： ada formal-verification spark-ada spark-2014

【解决方案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

【讨论】：

为什么 gnatprove 说当 X 为 2 且 Y 为 -2 时 X * Y 可能会溢出”我不明白。
我不会忽略最后一个值，因为它从 0 开始迭代。
@PoliteMan 我认为 Jim 试图帮助您将 for 循环简化为 For E of reverse A loop Y := Y * X + E;结束循环；尽管他建议在反向 A'Range 循环中使用 for I 的索引版本 Y := Y * X +A(I);结束循环；