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

#ada #formal-verification #spark-ada #spark-2014

#ada #формальная проверка #spark-ada #spark-2014 #spark-формальная проверка

Вопрос:

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

 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.

Я пишу свою функцию 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

1. Попробуйте запустить Rulehorner (1, (Integer'Last, Integer'Last)) ; это дает Constraint_Error .

2. @Simon Wright Есть ли у вас какие-либо идеи, как улучшить спецификацию и тело horner_rule с помощью spark, чтобы доказать все утверждения?

3. Я хочу сказать, что вы не можете доказать отсутствие исключений при существующем положении вещей, потому что есть входные данные, для которых эта функция будет вызывать исключения! Это ваша функция, вы могли бы помочь себе, указав, что она должна делать, предпочтительно в форме лучших предварительных условий и постусловия. Для начала можно было бы перевести на английский; понятия не имею.

Ответ №1:

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

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

 for I in reverse A'Range loop

1. Почему gnatprove говорит, что X * Y может переполниться, когда X равно 2, а Y равно -2 » Я не понимаю.

2. Я не игнорирую последнее значение, потому что оно повторяется с 0.

3. @PoliteMan Я думаю, Джим пытается помочь вам упростить ваш цикл for до чего-то вроде For E обратного цикла Y: = Y * X E; завершите цикл; Хотя он предлагал индексную версию for I в обратном цикле Y:= Y * X A (I); завершите цикл;