问题描述
我试图证明,我在数组中查找第二大值的算法可以正常工作。这是我的代码:
function FindMax2 (V : Vector) return Integer is
Max : Natural := 0;
SecondMax : Natural := 0;
begin
for I in V'Range loop
pragma Assert
(Max >= 0 and
SecondMax >= 0 and
V(I) > 0);
if V(I) > Max then
SecondMax := Max;
Max := V(I);
elsif V(I) /= Max and V(I) > SecondMax then
SecondMax := V(I);
end if;
pragma Loop_Invariant
(Max > SecondMax and
V(I) > 0 and
(for all J in V'First .. I => V(J) <= Max));
end loop;
return SecondMax;
end FindMax2;
这是我的前置和后置条件:
package Max2 with SPARK_Mode is
type Vector is array (Integer range <>) of Positive;
function FindMax2 (V : Vector) return Integer
with
Pre => V'First < Integer'Last and V'Length > 0,Post => FindMax2'Result >= 0 and
(FindMax2'Result = 0 or (for some I in V'Range => FindMax2'Result = V(I))) and
(if FindMax2'Result /= 0 then (for some I in V'Range => V(I) > FindMax2'Result)) and
(if FindMax2'Result = 0 then (for all I in V'Range => (for all J in V'Range => V(I) = V(J)))
else
(for all I in V'Range => (if V(I) > FindMax2'Result then (for all J in V'Range => V(J) <= V(I)))));
end Max2;
我现在被 GNATprove 的这条消息困住了:
max2.ads:8:17: medium: postcondition might fail (e.g. when FindMax2'Result = 1 and V = (others => 1) and V'First = 0 and V'Last = 0)
如果我没记错,它是指结果大于或等于 0 的第一个条件,那么为什么它把 1 作为反例呢?有什么办法可以证明这一点吗?
解决方法
我设法解决了我的问题。我对错误消息的理解是错误的,gnatprove 指的是整个后置条件语句。如果有人对解决方案感兴趣,我在循环不变式中添加了一些条件
pragma Loop_Invariant
(Max > SecondMax and
V(I) > 0 and
(for all J in V'First .. I => V(J) <= Max) and
(Max = 0 or (for some J in V'First .. I => Max = V(J))) and
(SecondMax = 0 or (for some J in V'First .. I => SecondMax = V(J))) and
(if SecondMax = 0 then (for all J in V'First .. I => (for all K in V'First .. I => V(J) = V(K)))
else (for all J in V'First .. I => (if V(J) > SecondMax then (for all K in V'First .. I => V(K) <= V(J))))));
,
请注意,实际答案是由 OP 自己 here 提供的。学分应该去那里。这只是我对这个好结果的评论的补充。
max2.ads
package Max2 with SPARK_Mode is
type Vector is array (Integer range <>) of Positive;
function All_Same (V : Vector) return Boolean is
(for all I in V'Range => (for all J in V'Range => V(I) = V(J)))
with Ghost;
function Elem_Of (V : Vector; X : Integer) return Boolean is
(for some I in V'Range => V (I) = X)
with Ghost;
function Is_Largest (V : Vector; X : Integer) return Boolean is
(Elem_Of (V,X) and (for all I in V'Range => V (I) <= X))
with Ghost;
function Is_Second_Largest (V : Vector; X : Integer) return Boolean is
(Elem_Of (V,X) and not Is_Largest (V,X) and
(for all I in V'Range => V(I) <= X or else Is_Largest (V,V (I))))
with Ghost;
pragma Annotate (GNATprove,Inline_For_Proof,All_Same);
pragma Annotate (GNATprove,Elem_Of);
pragma Annotate (GNATprove,Is_Largest);
pragma Annotate (GNATprove,Is_Second_Largest);
procedure FindMax2 (V : Vector; Found : out Boolean; Value : out Natural)
with Post => (if Found then Is_Second_Largest (V,Value) else All_Same (V));
end Max2;
max2.adb
package body Max2 with SPARK_Mode is
--------------
-- FindMax2 --
--------------
procedure FindMax2
(V : in Vector;
Found : out Boolean;
Value : out Natural)
is
L1 : Natural := 0;
L2 : Natural := 0;
begin
if V'Length > 1 then
for I in V'Range loop
if L1 < V(I) then
L2 := L1;
L1 := V(I);
elsif L2 < V(I) and V(I) < L1 then
L2 := V(I);
end if;
pragma Loop_Invariant
(L2 < L1);
pragma Loop_Invariant
(L1 = 0 or Elem_Of (V (V'First .. I),L1));
pragma Loop_Invariant
(L2 = 0 or Elem_Of (V (V'First .. I),L2));
pragma Loop_Invariant
(Is_Largest (V (V'First .. I),L1));
pragma Loop_Invariant
(if L2 = 0
then All_Same (V (V'First .. I))
else Is_Second_Largest (V (V'First .. I),L2));
end loop;
end if;
Found := (L2 > 0);
Value := L2;
end FindMax2;
end Max2;