Как использовать Assert и loop_invariants - PullRequest
Новая
       34

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

1 голос
/ 09 марта 2019

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

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

1 Ответ

3 голосов
/ 09 марта 2019

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

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

for I in reverse A'Range loop
...