小编Nes*_*001的帖子

我需要有关 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 的字符，但它没有解决问题。有谁有解决问题的方法吗？