Ada GNATprove Command_Line.Argument precondition fail

Question

I'm trying to write a simple verification code block to ensure the argument(Ada.Command_Line.Argument) and input from GetLine are valid, which in my case, I need all the characters in the input String to be numbers (0 to 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;

The program works perfectly fine. If I input ./main 01234 it will return aaaaa, and if I input ./main f00 it will return nothing. However, when I use GNATprove (in GPS -> SPARK -> Prove All), it gives me precondition might fail, cannot prove S(I) >= '0' (e.g. when I = 1 and user_str = (2 => '0', others => 'NUL')). I'm not sure why this happens since if the none digit character exists, the ToA procedure shouldn't be called.

Answer 1

I don't think you'll ever be able to prove this, since the call to CL.Argument might violate the function's precondition. You should do something like

User_Str : String := (if CL.Argument_Count > 0 then CL.Argument (1) else "");

You could use the full power of the SPARK language to simplify your code:

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);

eliminating the first if in Main, and the body of Toa could simply be

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

These get rid of unnecessary loops and the need to specify loop invariants to prove them, which might help your proof succeed.

Answer 2

I think Jeffrey’s answer looks great, but these changes to your code let proof succeed:

• make user_str start at index 1 (the loop invariant becomes more difficult without this),

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

• add a loop invariant, like 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');

The first change still has a problem, because we don’t know that Argument_Count is at least 1; this could be fixed by getting the argument in a declare block guarded by the check on Argument_Count = 1.

Answer 3

What seems missing is a loop invariant that shows the prover how the value of Flag (or All_Digits in the example below) relates to the part of the string that has been checked. In the example below, I refactored your example a little bit in order to isolate the code to be proved from the usage of the package Ada.Command_Line. This package has not been annotated and hence raises warnings during the proof session. The procedure Check_Argument itself can be proven in 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;

output (prover)

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