Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Liseq.adb Sprache: Ada

Original von: Isabelle^©

-------------------------------------------------------------------------------
-- Longest increasing subsequence of an array of integers
-------------------------------------------------------------------------------

package body Liseq is

   procedure Liseq_length(A: in Vector; L: in out Vector; maxi: out Integer)
   is
      maxj,i,j,pmax : Integer;
   begin
      L(0) := 1;
      pmax := 0;
      maxi := 1;
      i := 1;
      while i <= L'Last
        --# assert
        --#   (for all i2 in Integer range 0 .. i-1 =>
        --#      (L(i2) = Liseq_ends_at(A, i2))) and
        --#   L(pmax) = maxi and L(pmax) = Liseq_prfx(A, i) and
        --#   0 <= i and i <= L'Last+1 and 0 <= pmax and pmax < i and
        --#   A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
      loop
         if A(i) < A(pmax) then
            maxj := 0;
            j := 0;
            while j < i
              --# assert
              --#  (for all i2 in Integer range 0 .. i-1 =>
              --#     (L(i2) = Liseq_ends_at(A, i2))) and
              --#  L(pmax) = maxi and L(pmax) = Liseq_prfx(A, I) and
              --#  0 <= i and i <= L'Last and 0 <= pmax and pmax < i and
              --#  0 <= j and j <= i and
              --#  maxj = Max_ext (A, i, j) and
              --#  A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
            loop
               if (A(j) <= A(i) and
                     maxj < L(j)) then
                  maxj := L(j);
               end if;
               j := j+1;
            end loop;
            L(i) := maxj+1;
            if L(i) > maxi then
               maxi := maxi+1;
               pmax := i;
            end if;
         else
            maxi := maxi+1;
            L(i) := maxi;
            pmax := i;
         end if;
         i := i+1;
      end loop;
   end Liseq_length;
end Liseq;

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.