Ada SPARK 将字符串转换为整数

Question

我需要有关 Ada SPARK 的帮助。 我想将像“1”这样的字符串保存到整数变量中。背景：我想从命令行输入读取数字并将它们作为整数处理，并使用 SPARK Prove 检查程序。 这是一个最小的例子：

with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;

procedure Main is
   pragma SPARK_Mode;
   test_string : Unbounded_String;
   identifier : Integer;
begin

   test_string := To_Unbounded_String("1");
   identifier := Integer'Value(To_String(test_string));
   
end Main;

当我执行 SPARK Prove 时，我收到以下消息：“中：前提条件可能失败”。我已经实现了一个函数来检查 test_string 是否包含 0 - 9 的字符，但它没有解决问题。 有谁有办法解决这个问题吗？

Answer 1

我没有明确的答案，但我的初步观察如下。

SPARK 手册对于如何解释

'Value

以及属性的前提条件有点模糊。 SPARK RM 15.2.1 指出

'Value

属性有一个隐含的前提条件：

属性	SPARK 中允许	评论
S’价值	是的	隐式前提条件（Ada RM 3.5(55/3)）

没有解释“隐式前提条件”的含义，但参考了RM 3.5 (55/3)，而它又指向RM 3.5 (39.12/3)。后者指出：

[...] 如果对应的数值属于 S 类型的基范围，则该值就是结果；否则，将引发 Constraint_Error。 [...].

因此，前提条件可能必须防止

Constraint_Error

的可能发生。但如何呢？

继续阅读 GNATprove 开发人员指南的标量属性部分，可以阅读以下内容：

标量属性

图像和值，目前不解释它们：[...]

术语“解释”没有明确定义（根据我所能找到的），但可能表明 GNATprove 将（在此时）只是不“解释”关于

'Value

属性的使用。这似乎与以下事实相符：即使是该属性的最简单用法，即像

"1"

这样的静态字符串的转换，也无法得到证明。

因此，基于此，我的假设是，以 SPARK 目前的状态，你根本无法满足前提条件。 SPARK 允许使用

'Value

属性，并将添加一个“隐式”前提条件，以确保证明者始终会失败 除非 有人仔细查看了它，审查了代码，并签署了属性的使用（另请参阅SPARK 用户指南，第 7.3.4.1 节有关理由注释）：

main.adb

procedure Main with SPARK_Mode is
   X : Integer;
begin   
   X := Integer'Value("1");
   pragma Annotate
     (GNATprove, False_Positive,
      "precondition might fail", "reviewed by DeeDee");   
end Main;

输出（蚊虫证明）

$ gnatprove -Pdefault.gpr -j0 -u main.adb --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
Summary logged in [...]/obj/gnatprove/gnatprove.out

$ cat ./obj/gnatprove/gnatprove.out
Summary of SPARK analysis
=========================

-----------------------------------------------------------------------------------------
SPARK Analysis results        Total      Flow   CodePeer   Provers   Justified   Unproved
-----------------------------------------------------------------------------------------
Data Dependencies                 .         .          .         .           .          .
Flow Dependencies                 .         .          .         .           .          .
Initialization                    .         .          .         .           .          .
Non-Aliasing                      .         .          .         .           .          .
Run-time Checks                   .         .          .         .           .          .
Assertions                        .         .          .         .           .          .
Functional Contracts              1         .          .         .           1          .
LSP Verification                  .         .          .         .           .          .
Termination                       .         .          .         .           .          .
Concurrency                       .         .          .         .           .          .
-----------------------------------------------------------------------------------------
Total                             1         .          .         .    1 (100%)          .


max steps used for successful proof: 0

Analyzed 1 unit
in unit main, 1 subprograms and packages out of 1 analyzed
  Main at main.adb:1 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
   suppressed messages:
    main.adb:4:16: reviewed by DeeDee

Answer 2

您是否尝试过在转换为整数之前以及检查字符以确保它们都在“0”到“9”范围内之后添加断言？

示例：

procedure Main is
   pragma SPARK_Mode;
   test_string : String := "123";
   Number : Integer;
begin
   -- pragma assert using a quantified expression
   pragma Assert (for all I in test_string'Range => Test_string(I) in '0'..'9');
   Number := Integer'Value(Test_String);
end Main;

Answer 3

我真的没有看到任何方法可以做到这一点。您需要能够告诉证明者，输入字符串不仅包含整数的图像，而且表示的值在 Integer 范围内。类似的东西

if (for some I in Integer => I'Image = Input) then
   -- Use Integer'Value
else
   -- Error handling
end if;

这是行不通的。