我想写一个简单的验证代码块，以确保参数(Ada.Command_Line.Argument)和GetLine的输入是有效的，在我的例子中，我需要输入String中的所有字符都是数字(0到9)。
main.adb.Ada.Command_Line.Argument）和GetLine的输入都是有效的，在我的例子中，我需要所有的输入String中的字符都是数字（0到9）。
pragma SPARK_Mode (On);
with test_procedure;
with Ada.Command_Line;
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
procedure Main is
package CL renames Ada.Command_Line;
user_str : String := CL.Argument(1);
Flag : Boolean := False;
begin
if CL.Argument_Count = 1 then
for I in user_str'Range loop
case user_str(I) is
when '0'..'9' => Flag := True;
when others => Flag := False; exit;
end case;
end loop;
end if;
if Flag then
test_procedure.ToA(user_str);
Put(user_str);
end if ;
end Main;
test_procedure.ads:
package test_procedure with SPARK_Mode is
procedure ToA(S : in out String) with
Pre => (for all I in S'Range => S(I) >= '0' and S(I) <= '9');
end test_procedure;
test_procedure.adb
package body test_procedure with SPARK_Mode is
procedure ToA(S : in out String) is
begin
for I in S'Range loop
S(I) := 'a';
end loop;
end ToA;
end test_procedure;
程序运行得非常好。如果我输入 ./main 01234 它将返回 aaaaa如果我输入 ./main f00 它将什么也不返回，但当我使用GNATprove(在GPS -> SPARK -> Prove All中)时，它却什么也不返回。然而，当我使用GNATprove(在GPS -> SPARK -> Prove All中)时，它给我的结果是 precondition might fail, cannot prove S(I) >= '0' (e.g. when I = 1 and user_str = (2 => '0', others => 'NUL')). 我不知道为什么会发生这种情况，因为如果没有数字字符存在，ToA过程就不应该被调用。
似乎缺少的是一个 循环不变量 的值，说明了谚语中 Flag (或 All_Digits 在下面的例子中）涉及到字符串中被检查的部分。在下面的例子中，我对你的例子进行了一些重构，以便将要证明的代码与包的使用隔离开来。Ada.Command_Line. 这个包没有被注释，因此在证明过程中会发出警告。过程 Check_Argument 本身可以在GNAT CE 2020中得到证明。
main.adb
with Ada.Command_Line;
with Check_Argument;
procedure Main is
package CL renames Ada.Command_Line;
begin
if CL.Argument_Count = 1 then
Check_Argument (CL.Argument (1));
end if;
end Main;
check_argument.adb
with Ada.Text_IO; use Ada.Text_IO;
procedure Check_Argument (Arg : String) with SPARK_Mode is
procedure To_A (S : in out String) with
Pre => (for all I in S'Range => S(I) in '0' .. '9');
----------
-- To_A --
----------
procedure To_A (S : in out String) is
begin
for I in S'Range loop
S (I) := 'a';
end loop;
end To_A;
User_Str : String := Arg;
All_Digits : Boolean := False;
-- NOTE: All_Digits must be initialized as User_Str might have length 0.
begin
for I in User_Str'Range loop
All_Digits := User_Str (I) in '0'..'9';
exit when not All_Digits;
pragma Loop_Invariant
(for all J in User_Str'First .. I =>
User_Str (J) in '0' .. '9');
pragma Loop_Invariant (All_Digits);
end loop;
if All_Digits then
To_A (User_Str);
Put (User_Str);
end if;
end Check_Argument;
产出 (谚语)
check_argument.adb:6:40: info: index check proved
check_argument.adb:28:31: info: index check proved
check_argument.adb:32:10: info: loop invariant initialization proved
check_argument.adb:32:10: info: loop invariant preservation proved
check_argument.adb:33:22: info: index check proved
check_argument.adb:35:30: info: loop invariant initialization proved
check_argument.adb:35:30: info: loop invariant preservation proved
check_argument.adb:40:7: info: precondition proved
我想 杰弗里的回答 看上去很不错，但对你的代码进行的这些修改让证明成功了。
user_str 从索引1开始(如果不这样做，循环不变性就会变得更加困难)。Str : constant String := CL.Argument(1);
user_str : String (1 .. Str'Length) := Str;
for I in user_str'Range loop
pragma Loop_Invariant
(for all C of user_str (1 .. I - 1) => C in '0' .. '9');
第一个变化还是有问题的，因为我们不知道。Argument_Count 至少为1；这可以通过在一个 declare 堵截 Argument_Count = 1.
我不认为你能证明这一点，因为对 CL.Argument 的调用可能会违反函数的前提条件。你应该做一些类似于
User_Str : String := (if CL.Argument_Count > 0 then CL.Argument (1) else "");
你可以使用SPARK语言的全部功能来简化你的代码。
subtype Digit is Character range '0' .. '9';
Flag : constant Boolean := User_Str'Length > 0 and then
(for all I in User_Str'range => User_Str (I) in Digit);
去掉第一个 if 在美因，而图雅的身体可以简单地。
S := (S'range => 'a');
这些摆脱了不必要的循环和需要指定循环不变量来证明它们，这可能会帮助你的证明成功。