使用 SPARK 证明 Select Sort 算法

2024-05-20 • 问答

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

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: 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) 你有什么想法如何解决这个问题吗？

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

我还更改了 Sorted ghost 函数/谓词以仅将量化表达式应用于长度大于 1 的数组。这是为了防止出现溢出问题。对于长度为 0 或 1 的数组，函数根据定义返回 True，因为 (if False then <bool_expr>) 是 True（或 vacuously true，如果我没记错的话）。

所有 VC 都可以使用 gnatprove 进行排放/证明，该 $ gnatprove -Pdefault.gpr -j0 --report=all --level=1 随 GNAT/SPARK CE 2020 一起提供，级别为 1：

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

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;

selection.adb

let fetchMade = false;

class CampusList extends HTMLElement {
  connectedCallback() {
    if (!fetchMade) {
      console.log('fetch!');
      fetchMade = true;
    } else {
      console.log('do not fetch');
    }
  }
}

customElements.define('campus-list',CampusList);

使用 SPARK 证明 Select Sort 算法

kaiyum88 回答：使用 SPARK 证明 Select Sort 算法

大家都在问