使用 SPARK 证明 Select Sort 算法 [英] Proving Select Sort algorithm using SPARK

问题描述

我试图证明我在 Ada 中实现的 Select Sort 是正确的.我尝试了一些循环不变量，但使用 gnatprove 只能证明内循环的不变量:

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 告诉我selection.adb:15:14: medium: 循环不变量可能不会被任意迭代保留，不能证明 Sorted( A (A'First..I)) (例如，当 A = (-1 => 0, 0 => 0, 其他 => 1) 和 A'First = -1) 你有什么想法如何解决这个问题吗?

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?

推荐答案

我稍微修改了例程，在外循环中添加了两个循环不变量，并将它们全部移到循环的末尾.两个额外的循环不变量表明，正在处理的元素总是大于或等于已处理的元素，小于或等于尚未处理的元素.

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.

我还更改了 Sorted 鬼函数/谓词，以仅将量化表达式应用于长度大于 1 的数组.这是为了防止溢出问题.对于长度为 0 或 1 的数组，函数根据定义返回 True 为 (if False then ) is True(或 Truea href="https://en.wikipedia.org/wiki/Vacuous_truth" rel="nofollow noreferrer">完全正确，如果我没记错的话.

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

所有 VC 都可以使用 gnatprove 释放/证明，该代码随 GNAT/SPARK CE 2020 一起提供，级别为 1:

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;

这篇关于使用 SPARK 证明 Select Sort 算法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！