Ada GNATprove Command_Line.Argument 前置条件失败答案

【问题标题】：Ada GNATprove Command_Line.Argument precondition failAda GNATprove Command_Line.Argument 前置条件失败
【发布时间】：2020-06-04 02:15:00
【问题描述】：

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

main.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 过程。

【问题讨论】：

如果将前置条件更改为(for all I in S'range => S (I) in '0' .. '9')，会发生什么？这是一种更类似于 Ada 的表达方式。不过，鉴于失败的性质，它可能无济于事。

标签： command-line ada gnat spark-ada

【解决方案1】：

似乎缺少的是loop invariant，它向证明者展示了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

【讨论】：

【解决方案2】：

我认为Jeffrey’s answer 看起来不错，但是对代码的这些更改让证明成功：

使user_str从索引1开始（没有这个循环不变量变得更加困难），

Str : constant String := CL.Argument(1);
user_str : String (1 .. Str'Length) := Str;

添加循环不变量，如DeeDee's

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；这可以通过将参数放入由Argument_Count = 1 的检查保护的declare 块中来解决。

【讨论】：

【解决方案3】：

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

消除 Main 中的第一个 if，Toa 的主体可能只是

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

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

【讨论】：