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

您是否尝试过在转换为整数之前以及检查字符以确保它们都在“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;