1

我正在尝试编写一个简单的验证代码块以确保参数（Ada.Command_Line.Argument）和来自 GetLine 的输入是有效的，在我的情况下，我需要输入字符串中的所有字符都是数字（0 到 9 ）。

主.adb：

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 中）时，它给了我precondition might fail, cannot prove S(I) >= '0' (e.g. when I = 1 and user_str = (2 => '0', others => 'NUL')). 我不确定为什么会发生这种情况，因为如果没有数字字符存在，则不应调用 ToA 过程。

4

3 回答 3

2

我认为您永远无法证明这一点，因为对 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);

消除ifMain 中的第一个，Toa 的主体可以简单地

S := (S'range => 'a');

这些消除了不必要的循环以及指定循环不变量来证明它们的需要，这可能有助于您的证明成功。

于 2020-06-04T06:43:57.683 回答
2

似乎缺少的是一个循环不变量Flag，它向证明者显示（或在下面的示例中）的值如何与All_Digits已检查的字符串部分相关。在下面的示例中，我对您的示例进行了一些重构，以便将要证明的代码与 package 的使用区分开来Ada.Command_Line。这个包没有被注释，因此在证明过程中会发出警告。该程序Check_Argument本身可以在 GNAT CE 2020 中得到证明。

主文件

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
于 2020-06-04T06:33:11.647 回答
2

我认为Jeffrey 的回答看起来很棒，但是对代码的这些更改让证明成功：

  • 从user_str索引 1 开始（没有这个循环不变量变得更加困难），
Str : constant String := CL.Argument(1);
user_str : String (1 .. Str'Length) := Str;
  • 添加一个循环不变量，如DeeDee的
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由 check on 保护的块中来解决Argument_Count = 1。

于 2020-06-04T07:51:00.597 回答