"Утверждение может потерпеть неудачу", и предварительное условие не решает его
У меня есть функция, которая контролирует контролируемый сигнал, применяя простую проверку, находится ли сигнал в заданном диапазоне допуска. Функция называется is_within_limits, У меня есть вторая функция под названием is_within_expanded_limits это делает то же самое, но применяет коэффициент расширения (расширяет диапазон допуска) заранее к настроенным пределам. Пределы настроены в monitor.config посредством целевого значения и максимального отклонения от этого значения или нижнего и верхнего порогов. Перечень monitor.config.monitoring_mode указывает, как указан допустимый диапазон.
Посмотрите на код в первую очередь.
Спецификация
subtype Float_Signed1000 is Float range -1_000.0 .. 1_000.0;
subtype Float_Signed10000 is Float range -10_000.0 .. 10_000.0;
type Monitor_Config_T is record
monitoring_mode : Monitoring_Mode_T := mean_based;
mean : Float_Signed1000 := 0.0;
maximum_deviation : Float range Float'Small .. 1_000.0 := 100.0e-3;
lower_threshold : Float_Signed1000 := -100.0e-3;
upper_threshold : Float_Signed1000 := 100.0e-3;
settling_tolerance_expansion : Float range (1.0 + Float'Small) .. 2.0 := 1.2;
startup_time : Time_Span := Milliseconds (5);
settling_time : Time_Span := Milliseconds (2);
violation_time : Time_Span := Milliseconds (5);
retry_time : Time_Span := Milliseconds (100);
end record;
type Monitor_T is record
config : Monitor_Config_T;
timer : Time_Span := Milliseconds (0);
current_state : Monitor_State_T := reset;
next_state : Monitor_State_T := reset;
end record;
function is_within_expanded_limits (monitor : in Monitor_T;
signal_value : in Float_Signed1000)
return Boolean
with Pre => (if monitor.config.monitoring_mode = mean_based then
monitor.config.maximum_deviation > 0.0)
and then (if monitor.config.monitoring_mode = threshold_based then
monitor.config.lower_threshold <
monitor.config.upper_threshold)
and then monitor.config.settling_tolerance_expansion > 1.0;
Реализация
function is_within_expanded_limits (monitor : in Monitor_T;
signal_value : in Float_Signed1000)
return Boolean is
within_expanded_limits : Boolean := False;
expanded_lower_threshold : Float Float_Signed10000;
expanded_upper_threshold : Float Float_Signed10000;
begin
case monitor.config.monitoring_mode is
when mean_based =>
if abs (monitor.config.mean - signal_value) <=
(monitor.config.maximum_deviation *
monitor.config.settling_tolerance_expansion) then
within_expanded_limits := True;
end if;
when threshold_based =>
-- Added due to recommendation by Jacob Sparre Andersen
-- Assertion is proved successfully
-- pragma Assert (monitor.config.lower_threshold < monitor.config.upper_threshold);
-- Added due to recommendation by Martin Becker
-- Adding this assumption still causes the assertion to fail
-- pragma Assume (monitor.config.lower_threshold = 10.0);
-- Adding this assumption still causes the assertion to fail
-- pragma Assume (monitor.config.upper_threshold = 11.0);
-- Replacing the assumption with this one results in the assertion being proved
-- pragma Assume (monitor.config.upper_threshold = 20.0);
-- Calculate expanded thresholds
if monitor.config.lower_threshold >= 0.0 then
expanded_lower_threshold := monitor.config.lower_threshold /
monitor.config.settling_tolerance_expansion;
else
expanded_lower_threshold := monitor.config.lower_threshold *
monitor.config.settling_tolerance_expansion;
end if;
if monitor.config.upper_threshold >= 0.0 then
expanded_upper_threshold := monitor.config.upper_threshold *
monitor.config.settling_tolerance_expansion;
else
expanded_upper_threshold := monitor.config.upper_threshold /
monitor.config.settling_tolerance_expansion;
end if;
-- @TODO why does this assertion fail?
pragma Assert (expanded_lower_threshold < expanded_upper_threshold);
-- Check limits with expanded thresholds
if signal_value >= expanded_lower_threshold and signal_value <=
expanded_upper_threshold then
within_expanded_limits := True;
end if;
end case;
return within_expanded_limits;
end is_within_expanded_limits;
Моя проблема в том, что утверждение pragma Assert (expanded_lower_threshold < expanded_upper_threshold) помечен как может потерпеть неудачу, и я не понимаю, почему. Я добавил это утверждение, чтобы проверить, что мой код не делает ничего странного, как инвертирование отношения нижнего и верхнего порога, а в первую очередь для проверки утверждений. Предварительное условие monitor.config.lower_threshold < monitor.config.upper_threshold в сочетании с кодом, который рассчитывает expanded_lower_threshold а также expanded_upper_threshold должен гарантировать, что утверждение всегда верно. Где проблема и как я могу это исправить?
1 ответ
Я предполагаю, что ваши пруверы просто столкнулись с таймаутом. Я попробовал ваш пример, и вот что случилось со мной.
Обычно пользовательский интерфейс не различает разные причины неудачных доказательств. Если вы сталкиваетесь с тайм-аутом и не замечаете этого, то кажется, что с вашим кодом что-то не так, хотя, возможно, это не так. Поскольку вы должны использовать GNATprove (в данный момент другого инструмента нет), перейдите в папку сборки и найдите подпапку с именем "gnatprove". Там вы найдете файл с именем your_package_name.spark. Это формат JSON, который дает вам информацию о том, что действительно сообщили проверяющие. Я уверен, что вы найдете там тайм-аут или ограничение шага. Я думаю, что ваш код может быть бездефектным, как я это уточню через минуту.
Но, прежде всего, ваш код не компилируется. Вы должны использовать правильный тип, чтобы определить диапазон параметра signal_value в функции is_within_expanded_limits, Поскольку диапазон одинаковый, вы можете использовать Float_Signed1000, В качестве альтернативы, добавьте предварительное условие (но тип лучше, так как тогда вызывающие, которые не находятся в SPARK_Mode, получают некоторую проверку типа / диапазона).
Затем рассмотрите возможность изменения сравнения на "<=", поскольку возможно, что ошибки округления опровергают строгий порядок. Я не уверен, является ли это проблематичным в этом случае, но имейте в виду, что SPARK моделирует вычисления, совместимые с IEEE754, и там может иметь значение, есть ли у вас число 1,2 (которое не может быть точно представлено), или 1,25 (которое может), Таким образом, я сделал это небольшое изменение в вашем коде.
Теперь вернемся к моему утверждению, что ваш код мог быть верным, несмотря на неудачные доказательства. Добавьте это в начало вашего дела:
pragma Assume (monitor.config.lower_threshold = 10.0);
Предупреждение: не используйте допустимые прагмы, кроме как для выяснения причины неудачи доказательства. Вещи могут пойти ужасно неправильно, если они используются неправильно.
Теперь выберите самый медленный режим для проверки, и ваше утверждение подтвердится (у проверяющего меньше "приказов" для проверки). Вы можете изменить значение в операторе предположения по своему усмотрению, но будьте осторожны, чтобы значение соответствовало диапазонам типов и предварительным условиям, в противном случае все будет доказано неверно (например, попробуйте Float'Last, а затем поместите pragma assert (False) сразу после принятия) Если что-то не доказано, пойди и посмотри почему, как описано выше. Нет смысла менять ваш код, пока вы не узнаете, что проверщик действительно пришел к выводу.
Вы можете попробовать библиотеку лемм SPARK, которая может включать такие упрямые доказательства: http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-using-the-lemma-library