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

Answer 2

请注意，实际答案是由 OP self 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, Inline_For_Proof, Elem_Of);
   pragma Annotate (GNATprove, Inline_For_Proof, Is_Largest);
   pragma Annotate (GNATprove, Inline_For_Proof, 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;