Ada 中数组最大

Question

如何检查某个值是否是数组中最大的元素？这是 Ada 语言。我有查找最大元素的函数，并且它有效。现在我想运行一个后置条件来检查该值是否是最大的。

Answer 1

循环遍历数组，如果找到更大的元素或没有找到相等的元素，则会失败？

function Check_Largest (In_Array : Array_Type; Value : Element_Type)
  return Boolean
is
   Matched : Boolean := False;
begin
   for J in In_Array'Range loop
      if In_Array (J) > Value then
         return False;
      elsif In_Array (J) = Value then
         Matched := True;
      end if;
   end loop;
   return Matched;
end Check_Largest;

在 2020 年、Ada 2012 之后重新审视这一点，一对量词可能会起到作用；请参阅 Largest_Member 的后置条件：

procedure Largest
with SPARK_Mode
is
   type Arr is array (Positive range <>) of Natural;

   function Largest_Member (Of_Array : Arr) return Natural
   with
     Pre => Of_Array'Length > 0,
     Post =>
       (for all E of Of_Array => E <= Largest_Member'Result)
       and
       (for some E of Of_Array => E = Largest_Member'Result);

   function Largest_Member (Of_Array : Arr) return Natural is
      Result : Integer := -1;
   begin
      for J in Of_Array'Range loop
         if Of_Array (J) > Result then
            Result := Of_Array (J);
         end if;
         pragma Loop_Invariant
           ((for all F of Of_Array (Of_Array'First .. J) => F <= Result)
            and
            (for some F of Of_Array (Of_Array'First .. J) => F = Result));
      end loop;
      return Result;
   end Largest_Member;
begin
   null;
end Largest;