Proving Select Sort algorithm using SPARK

Question

I am trying to prove that my implementation of Select Sort in Ada is correct. I have tried a few loop invariants, but using gnatprove only proves inner loop's invariant:

package body Selection with SPARK_Mode is

procedure Sort (A : in out Arr) is
    I: Integer := A'First;
    J: Integer;
    Min_Idx: Integer;
    Tmp: Integer;
begin
    while I < A'Last loop

        pragma Loop_Invariant
            (Sorted( A (A'First .. I) ));

        Min_Idx := I;
        J := I + 1;

        while J <= A'Last loop

            if A (J) < A (Min_Idx) then
                Min_Idx := J;
            end if;

            pragma Loop_Invariant
                (for all Index in I .. J => (A (Min_Idx) <= A (Index)));

            J := J + 1;
        end loop;

        Tmp := A (Min_Idx);
        A (Min_Idx) := A (I);
        A (I) := Tmp;

        I := I + 1;

    end loop;
end Sort;
end Selection;

package Selection with SPARK_Mode is
    type Arr is array (Integer range <>) of Integer;

    function Sorted (A : Arr) return Boolean
    is (for all I in A'First .. A'Last - 1 => A(I) <= A(I + 1))
    with
        Ghost,
        Pre => A'Last > Integer'First;

    procedure Sort (A : in out Arr)
    with
        Pre => A'First in Integer'First + 1 .. Integer'Last - 1 and
            A'Last in Integer'First + 1 .. Integer'Last - 1,
        Post => Sorted (A);

end Selection;

Gnatprove tells me selection.adb:15:14: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove Sorted( A (A'First..I)) (e.g. when A = (-1 => 0, 0 => 0, others => 1) and A'First = -1) Do you have any ideas how to solve this problem?

Answer 1

I reworked the routine a little bit, added two loop invariants to the outer loops and moved all of them to the end of the loop. The two additional loop invariants state that the element being processed is always greater-than or equal-than those that have already been processed and less-than or equal-than those yet to be processed.

I also changed the Sorted ghost function / predicate to only apply the quantified expression to arrays with length greater than 1. This is to prevent problems with overflow. For arrays of length 0 or 1, the function returns True by definition as (if False then <bool_expr>) is True (or vacuously true, if I remember correctly).

All VCs can be discharged/proved with gnatprove that ships with GNAT/SPARK CE 2020 at level 1:

$ gnatprove -Pdefault.gpr -j0 --report=all --level=1

selection.ads

package Selection with SPARK_Mode is
   
   type Arr is array (Integer range <>) of Integer;

   function Sorted (A : Arr) return Boolean is
     (if A'Length > 1 then
         (for all I in A'First + 1 .. A'Last => A (I - 1) <= A (I)))
       with Ghost;
         
   procedure Sort (A : in out Arr)
     with Post => Sorted (A);

end Selection;

selection.adb

package body Selection with SPARK_Mode is
   
   ----------
   -- Sort --
   ----------
   
   procedure Sort (A : in out Arr) is
      M : Integer;      
   begin
      if A'Length > 1 then
         for I in A'First .. A'Last - 1 loop
         
            M := I;
         
            for J in I + 1 .. A'Last loop            
               if A (J) <= A (M) then
                  M := J;
               end if;
            
               pragma Loop_Invariant (M in I .. J);            
               pragma Loop_Invariant (for all K in I .. J => A (M) <= A (K));
            
            end loop;
            
            declare
               T : constant Integer := A (I);
            begin
               A (I) := A (M);
               A (M) := T;
            end;
                  
            --  Linear incremental sorting in ascending order.
            pragma Loop_Invariant (for all K in A'First .. I => A (K) <= A (I));
            pragma Loop_Invariant (for all K in I .. A'Last  => A (I) <= A (K));
         
            pragma Loop_Invariant (Sorted (A (A'First .. I)));         

         end loop;
      end if;
   end Sort;
   
end Selection;