[Spark2014-discuss] Loop invariant for bubble sort

Claire Dross dross at adacore.com
Fri Jul 4 16:27:31 CEST 2014


Le 02/07/2014 23:33, Yannick Moy a écrit :
> -- Hugues Jérôme (2014-07-02)
>> Hi,
>>
>> I’m trying to prove a bubble sort, and face some issues on invariants (an area where I need some more insights than I expected). I took for granted from Claire on her last blog post that proving a sort being correct was “easy", and tried, but failed :(
> Hi Jérôme,
>
> The blog post says that proving sorting is "easier" than proving that the result is a permutation of the input, but not that it's "easy". So don't feel bad! :)
>
>
Hi Jérôme,

I have completed the selection sort example to also prove that the 
resulting array is sorted. It still proves with CVC4 and alt-ergo with a 
timeout of 5 seconds.

Hope this helps,

Claire
-------------- next part --------------
package body Sort
   with SPARK_Mode
is

   -----------------------------------------------------------------------------
   procedure Swap (Values : in out Nat_Array;
                   X      : in     Positive;
                   Y      : in     Positive)
   with
      Pre  => (X in Values'Range and then
                  Y in Values'Range and then
                  X /= Y),

       Post => Values =
         Set (Set (Values'Old, X, Values'Old (Y)), Y, Values'Old (X))
   is
      Temp : Integer;

      --  Ghost variables
      Init   : constant Nat_Array (Values'Range) := Values;
      Interm : Nat_Array (Values'Range);

   begin
      Temp       := Values (X);
      Values (X) := Values (Y);

      --  Ghost code
      pragma Assert (Values = Set (Init, X, Init (Y)));
      Interm := Values;

      Values (Y) := Temp;

      --  Ghost code
      pragma Assert (Values = Set (Interm, Y, Init (X)));
   end Swap;

   -- Finds the index of the smallest element in the array
   function Index_Of_Minimum (Values : in Nat_Array)
                              return Positive
     with
       Pre  => Values'Length > 0,
       Post => Index_Of_Minimum'Result in Values'Range and then
       (for all I in Values'Range =>
          Values (Index_Of_Minimum'Result) <= Values (I))
   is
      Min : Positive;
   begin
      Min := Values'First;
      for Index in Values'Range loop
         if Values (Index) < Values (Min) then
            Min := Index;
         end if;
         pragma Loop_Invariant
           (Min in Values'Range and then
              (for all I in Values'First .. Index =>
                   Values (Min) <= Values (I)));
      end loop;
      return Min;
   end Index_Of_Minimum;

   procedure Selection_Sort (Values : in out Nat_Array) is
      Smallest : Positive;  -- Index of the smallest value in the unsorted part

      --  Ghost variable
      Previous : Nat_Array (Values'Range);

      --  Ghost procedure
      procedure Prove_Swap_Perm (Values, Next : Nat_Array; X, Y : Index) with
        Pre  => X in Values'Range and then Y in Values'Range and then
           Next = Set (Set (Values, X, Values (Y)), Y, Values (X)),
        Post => Is_Perm (Values, Next) is
      begin
         for E in Natural loop
            Occ_Set (Values, X, Values (Y), E);
            Occ_Set (Set (Values, X, Values (Y)), Y, Values (X), E);
            Occ_Eq (Next, Set (Set (Values, X, Values (Y)), Y, Values (X)), E);
            pragma Loop_Invariant
              (for all F in Natural'First .. E =>
                 Occ (Values, F) = Occ (Next, F));
         end loop;
      end Prove_Swap_Perm;
   begin
      if Values'Length = 0 then
         return;
      end if;

      for Current in Values'First .. Values'Last - 1 loop
         Smallest := Index_Of_Minimum (Values (Current .. Values'Last));

         if Smallest /= Current then

            --  Ghost code
            Previous := Values;

            Swap (Values => Values,
                  X      => Current,
                  Y      => Smallest);

            --  Ghost code
            Prove_Swap_Perm (Previous, Values, Current, Smallest);
         end if;

         pragma Loop_Invariant
           (for all I in Values'First .. Current =>
              (for all J in I + 1 .. Values'Last =>
                   Values (I) <= Values (J)));
         pragma Loop_Invariant (Is_Perm (Values'Loop_Entry, Values));
      end loop;

   end Selection_Sort;

end Sort;
-------------- next part --------------
with Perm; use Perm;

package Sort with SPARK_Mode is

   -- Sorts the elements in the array Values in ascending order
   procedure Selection_Sort (Values : in out Nat_Array)
     with
       Post => Is_Perm (Values'Old, Values) and then
     (if Values'Length > 0 then
        (for all I in Values'First .. Values'Last - 1 =>
             Values (I) <= Values (I + 1)));
end Sort;


More information about the Spark2014-discuss mailing list