Ada SPARK convert string to integer

Question

I need help some help with Ada SPARK. I would like to save a string like "1" into an integer variable. Background: I would like to read numbers from the command line input and process them as integers and check the program with SPARK Prove. Here's a minimal example:

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;

When I execute SPARK Prove I get the following message: "medium: precondition might fail". I already implemented a function which checks whether the test_string consists of characters from 0 - 9, but it didn't solved the issue. Does anyone has a solution how to fix the problem?

Answer 1

Have you tried adding an assertion before your conversion to an Integer and after checking the characters to ensure they are all in the range of '0' through '9'?

Example:

procedure Main is
   pragma SPARK_Mode;
   test_string : String := "123";
   Number : Integer;
begin
   -- pragma assert using a quantified expression
   pragma Assert (for all I in test_string'Range => Test_string(I) in '0'..'9');
   Number := Integer'Value(Test_String);
end Main;

Answer 2

I do not have a definitive answer, but my initial observation is as follows.

The SPARK manuals are a little bit vague on how 'Value is interpreted and what this precondition on the attribute looks like. The SPARK RM 15.2.1 states that the 'Value attribute has an implicit precondition:

Attribute	Allowed in SPARK	Comment
S’Value	Yes	Implicit precondition (Ada RM 3.5(55/3))

What "implicit precondition" means is not explained, but a reference is is given to RM 3.5 (55/3) which in turn points to RM 3.5 (39.12/3). The latter states that:

[...] and if the corresponding numeric value belongs to the base range of the type of S, then that value is the result; otherwise, Constraint_Error is raised. [...].

So, the precondition will likely have to prevent the possible occurrence of a Constraint_Error. But how?

Reading on in the GNATprove developer's guide, section scalar attributes, one can read the following:

Scalar Attributes

Image and Value, they are not interpreted currently: [...]

The term "interpreted" is not defined explicitly (from what I could find), but probably indicates that GNATprove will (at this point in time) just not "reason" about the usage of the 'Value attribute. This seems consistent with the fact that even the simplest usage of the attribute, the conversion of a static string like "1", cannot be proven.

So, based on this, my hypothesis is that, with the current state of SPARK, you simply cannot satisfy the precondition. SPARK allows the usage of the 'Value attribute and will add an "implicit" precondition to ensure that the prover will always fail unless someone had a good look at it, reviewed the code, and signed off the attribute's usage (see also SPARK User's Guide, section 7.3.4.1 on justification annotations):

main.adb

procedure Main with SPARK_Mode is
   X : Integer;
begin   
   X := Integer'Value("1");
   pragma Annotate
     (GNATprove, False_Positive,
      "precondition might fail", "reviewed by DeeDee");   
end Main;

output (gnatprove)

$ gnatprove -Pdefault.gpr -j0 -u main.adb --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
Summary logged in [...]/obj/gnatprove/gnatprove.out

$ cat ./obj/gnatprove/gnatprove.out
Summary of SPARK analysis
=========================

-----------------------------------------------------------------------------------------
SPARK Analysis results        Total      Flow   CodePeer   Provers   Justified   Unproved
-----------------------------------------------------------------------------------------
Data Dependencies                 .         .          .         .           .          .
Flow Dependencies                 .         .          .         .           .          .
Initialization                    .         .          .         .           .          .
Non-Aliasing                      .         .          .         .           .          .
Run-time Checks                   .         .          .         .           .          .
Assertions                        .         .          .         .           .          .
Functional Contracts              1         .          .         .           1          .
LSP Verification                  .         .          .         .           .          .
Termination                       .         .          .         .           .          .
Concurrency                       .         .          .         .           .          .
-----------------------------------------------------------------------------------------
Total                             1         .          .         .    1 (100%)          .


max steps used for successful proof: 0

Analyzed 1 unit
in unit main, 1 subprograms and packages out of 1 analyzed
  Main at main.adb:1 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
   suppressed messages:
    main.adb:4:16: reviewed by DeeDee

Answer 3

I don't really see any way to do this. You need to be able to tell the prover that the input string not only contains the image of an integer, but that the value represented is in the range of Integer. Something like

if (for some I in Integer => I'Image = Input) then
   -- Use Integer'Value
else
   -- Error handling
end if;

which is unworkable.