SPARK problem with unconstrained arrays

SPARK problem with unconstrained arrays

[Maciej Sobczak]

I would like to play a bit with unconstrained arrays in SPARK and I found the following problem.
Consider the package specs:

pragma SPARK_Mode;

package My_Package is

    type Index is range 1 .. 10;
    type My_Array is array (Index range <>) of Integer;
    
    procedure Find_Min (A : in My_Array; I : out Index)
        with Post =>
             (I in A'Range and
                (for all J in A'Range =>
                    A (I) <= A (J)));

end My_Package;

The Find_Min procedure is supposed to find the index of the smallest element in the array.
The package body is:

pragma SPARK_Mode;

package body My_Package is

    procedure Find_Min (A : in My_Array; I : out Index) is
        Last_Min : Integer;
    begin
        I := A'First; -- line 8
        Last_Min := A (A'First); -- line 9
        
        for J in A'First + 1 .. A'Last loop

            if A (J) < Last_Min then
                I := J;
                Last_Min := A (J);
            end if;

            pragma Loop_Invariant
                (for all K in A'First .. J =>
                    I in A'First .. J and Last_Min = A (I) and Last_Min <= A (K));
        end loop;
    end Find_Min;
    
end My_Package;

GNATprove says:

C:\maciej\temp\spark>gnatprove -Ptest -q
my_package.adb:8:15: warning: range check might fail
my_package.adb:9:25: warning: array index check might fail
my_package.ads:10:14: warning: postcondition might fail
gprbuild: *** compilation phase failed
gnatprove: error during generation and proof of VCs, aborting.

How is it possible that VC at line 8 is not discharged? According to ARM:

"A'First denotes the lower bound of the first index range; its type is the corresponding index type."

and the index type (Index) happens to be the same on both sides of the assignment [*].

Curiously, VC at line 9 also fails, this time with even more surprising A (A'First).


[*] Or not. The ARM also says that unconstrained array is defined with the subtype_mark as an index, which might be a hint that the actual type in question is A'Base, which in this case is wider than 1..10. In other words, A'First is of the type that is wider than A'Range.
Adding this just before line 8 helps:

        pragma Assume (A'First in A'Range);

but seems to be an overkill (not because it's a lot of typing, but because it undermines the trust in the tool) and I would expect it to be deduced automagically.

What are your thoughts on this?

-- 
Maciej Sobczak * http://www.inspirel.com/

Re: SPARK problem with unconstrained arrays

[Maciej Sobczak]

> Adding this just before line 8 helps:
> 
>         pragma Assume (A'First in A'Range);

After some exploration I can answer my own question: empty slices.

Solution: add precondition to the Find_Min procedure:

    procedure Find_Min (A : in My_Array; I : out Index)
        with Pre => A'First <= A'Last,
             -- ...

The earliest added value of formal methods (and SPARK in particular) is in showing us how much we assume of what might not be actually true...

-- 
Maciej Sobczak * http://www.inspirel.com/

Re: SPARK problem with unconstrained arrays

[Jacob Sparre Andersen]

Maciej Sobczak <see.my.homepage@gmail.com> writes:

>     procedure Find_Min (A : in My_Array; I : out Index)
>         with Pre => A'First <= A'Last,
>              -- ...

Wouldn't "A'Length >= 1" be more readable?

Greetings,

Jacob
-- 
"The butcher backed into the meat grinder and got a little behind
 in his work."

Re: SPARK problem with unconstrained arrays

[Maciej Sobczak]

> >     procedure Find_Min (A : in My_Array; I : out Index)
> >         with Pre => A'First <= A'Last,
> >              -- ...
> 
> Wouldn't "A'Length >= 1" be more readable?

I would like to write:

not A'Empty

:-)

A'Length introduces new name and one constant into the whole mix, but indeed might be easier to read.

-- 
Maciej Sobczak * http://www.inspirel.com

Re: SPARK problem with unconstrained arrays

[Shark8]

> A'Length introduces new name and one constant into the whole mix, but indeed might be easier to read.

I prefer A'Length in Positive.

Re: SPARK problem with unconstrained arrays

[phil.clayton]

On Tuesday, 3 March 2015 09:41:35 UTC, Maciej Sobczak  wrote:
> After some exploration I can answer my own question: empty slices.
> 
> Solution: add precondition to the Find_Min procedure:
> 
>     procedure Find_Min (A : in My_Array; I : out Index)
>         with Pre => A'First <= A'Last,
>              -- ...

Interestingly, this precondition was known to be necessary before your package body even existed: in the postcondition, there is no way that the predicate
  I in A'Range
could be satisfied if A is empty (and A does not change because it is an 'in' parameter).

There is a theoretical method for determining a 'minimum' precondition of a specification - that is, the condition under which the specification is achievable.  Just existentially quantify over the 'changed' variables, in your case I:

  ∃ I : Index ⦁
    I ∈ A'Range ∧
      (∀ J : A'Range ⦁ A (I) ≤ A (J)) 

That's a predicate whose only free variable is A, so it says something about A.  Unfortunately, it's not obvious what.  That's probably equivalent to A is not empty in the context of A : My_Array.  In one direction the proof is trivial but in the other, you probably have to start by showing that a non-empty set of integers has a least element...  It's this sort of thing that gave formal methods a bad name.

Phil