问题描述
我试图证明我在 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);