Как мне убедить GNATprove, что вызов Integer'Value для одного и того же ввода дважды должен давать один и тот же результат?

При двукратном анализе целого числа из одной и той же строки GNATprove не допускает, чтобы одно и то же целое число производилось дважды. Как мне это исправить?

Основной файл:

with String_Problem;

procedure Eq_Test is
begin
   String_Problem.String_Equal("4456");
end Eq_Test;

String_Problem.ads:

package String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   with
       Ghost;
end String_Problem;

String_Problem.adb:

package body String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   is
      X1 : Integer;
      X2 : Integer;
   begin
      X1 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      X2 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      pragma Assert (X1 = X2);
   end String_Equal;
end String_Problem;

Выход GNATProve:

alr gnatprove
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

string_problem.adb:16:22: medium: assertion might fail
   16 |      pragma Assert (X1 = X2);
      |                     ^~~~~~~
Summary logged in [path]/gnatprove/gnatprove.out

Атрибут «Значение» был подтвержден в SPARK?

Jim Rogers 09.11.2022 03:57

@JimRogers Боюсь, я не понимаю, что ты имеешь в виду

user3519580 09.11.2022 15:09

Доказали ли компиляторы AdaCore атрибут «Value»? GnatProve может быть не в состоянии определить, что значение всегда возвращает один и тот же результат для согласованного значения параметра.

Jim Rogers 09.11.2022 15:40

Ах, я только что забрал Ada/SPARK, и поэтому понятия не имею, как это узнать!

user3519580 09.11.2022 15:53

Конечно, SPARK может доказать следующее: X1 := Integer'Value(A); Х2 := Х1; прагма Assert (X1 = X2);

Jim Rogers 09.11.2022 17:05
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
5
130
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Возможно, пока нет приемлемого ответа.

Есть очень похожий вопрос: Ada SPARK преобразовать строку в целое число

Обычно GNATProve может проверять такие вещи. Следующий код обычно не вызывает проблем:

X1 := function_1(A)
X2 := function_1(A)
pragma Assert (X1 = X2)

Это возможно даже для GNATProve, если функция_1 не может быть проверена или если функция_1 имеет открытые проблемы или даже не реализована. GNATProve должен знать только поток данных функции_1. Для функций это понятно. SPARK (не Ada) требует, чтобы функции не имели побочных эффектов. Зная это, становится очевидным, что два вызова дают один и тот же результат. И это также ясно для GNATProve.

Но у тебя нет функций. У вас есть атрибут Value. И, как показывает другой вопрос, у GNATProve есть ограничения, когда дело доходит до атрибута Value. Похоже, что GNATProve не использует тот факт, что его двойной вызов дает один и тот же результат. GNATProve, похоже, отказывается включать какие-либо сведения об атрибуте value.

Поскольку это ограничение, вы ничего не сможете с этим поделать.

Либо вы ставите pragma Assume(X1 = X2);, либо пишете функцию вокруг атрибута Value. Если это вариант для вас, ваш код будет таким:

package body Show_Runtime_Errors is

   function Integer_Value(A : in String) return Integer is
     (Integer'Value(A));
   pragma Annotate(Gnatprove, False_Positive, "precondition might fail", "GNATProve limitation");

   procedure String_Equal
     (A : String)
   is
      X1 : Integer;
      X2 : Integer;
   begin
      X1 := Integer_Value (A);
      X2 := Integer_Value (A);
      pragma Assert (X1 = X2);
   end String_Equal;
   
end Show_Runtime_Errors;

Другие вопросы по теме