Ada GNAT 证明 1 不是 >= 0

Question

我试图证明，我在数组中查找第二大值的算法可以正常工作。这是我的代码:

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作为反例呢？有什么办法可以证明这一点吗？

Answer 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))))));