src/HOL/SPARK/Examples/Liseq/Liseq.adb
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/Liseq/Liseq.adb	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,55 @@
     1.4 +-------------------------------------------------------------------------------
     1.5 +-- Longest increasing subsequence of an array of integers
     1.6 +-------------------------------------------------------------------------------
     1.7 +
     1.8 +package body Liseq is
     1.9 +
    1.10 +   procedure Liseq_length(A: in Vector; L: in out Vector; maxi: out Integer)
    1.11 +   is
    1.12 +      maxj,i,j,pmax : Integer;
    1.13 +   begin
    1.14 +      L(0) := 1;
    1.15 +      pmax := 0;
    1.16 +      maxi := 1;
    1.17 +      i := 1;
    1.18 +      while i <= L'Last
    1.19 +        --# assert
    1.20 +        --#   (for all i2 in Integer range 0 .. i-1 =>
    1.21 +        --#      (L(i2) = Liseq_ends_at(A, i2))) and
    1.22 +        --#   L(pmax) = maxi and L(pmax) = Liseq_prfx(A, i) and
    1.23 +        --#   0 <= i and i <= L'Last+1 and 0 <= pmax and pmax < i and
    1.24 +        --#   A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
    1.25 +      loop
    1.26 +         if A(i) < A(pmax) then
    1.27 +            maxj := 0;
    1.28 +            j := 0;
    1.29 +            while j < i
    1.30 +              --# assert
    1.31 +              --#  (for all i2 in Integer range 0 .. i-1 =>
    1.32 +              --#     (L(i2) = Liseq_ends_at(A, i2))) and
    1.33 +              --#  L(pmax) = maxi and L(pmax) = Liseq_prfx(A, I) and
    1.34 +              --#  0 <= i and i <= L'Last and 0 <= pmax and pmax < i and
    1.35 +              --#  0 <= j and j <= i and
    1.36 +              --#  maxj = Max_ext (A, i, j) and
    1.37 +              --#  A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
    1.38 +            loop
    1.39 +               if (A(j) <= A(i) and
    1.40 +                     maxj < L(j)) then
    1.41 +                  maxj := L(j);
    1.42 +               end if;
    1.43 +               j := j+1;
    1.44 +            end loop;
    1.45 +            L(i) := maxj+1;
    1.46 +            if L(i) > maxi then
    1.47 +               maxi := maxi+1;
    1.48 +               pmax := i;
    1.49 +            end if;
    1.50 +         else
    1.51 +            maxi := maxi+1;
    1.52 +            L(i) := maxi;
    1.53 +            pmax := i;
    1.54 +         end if;
    1.55 +         i := i+1;
    1.56 +      end loop;
    1.57 +   end Liseq_length;
    1.58 +end Liseq;