src/HOL/SPARK/Examples/Liseq/Liseq.adb
author wenzelm
Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 41561 d1318f3c86ba
permissions -rw-r--r--
tuned NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     1
-------------------------------------------------------------------------------
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     2
-- Longest increasing subsequence of an array of integers
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     3
-------------------------------------------------------------------------------
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     4
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     5
package body Liseq is
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     6
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     7
   procedure Liseq_length(A: in Vector; L: in out Vector; maxi: out Integer)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     8
   is
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     9
      maxj,i,j,pmax : Integer;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    10
   begin
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    11
      L(0) := 1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    12
      pmax := 0;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    13
      maxi := 1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    14
      i := 1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    15
      while i <= L'Last
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    16
        --# assert
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    17
        --#   (for all i2 in Integer range 0 .. i-1 =>
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    18
        --#      (L(i2) = Liseq_ends_at(A, i2))) and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    19
        --#   L(pmax) = maxi and L(pmax) = Liseq_prfx(A, i) and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    20
        --#   0 <= i and i <= L'Last+1 and 0 <= pmax and pmax < i and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    21
        --#   A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    22
      loop
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    23
         if A(i) < A(pmax) then
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    24
            maxj := 0;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    25
            j := 0;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    26
            while j < i
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    27
              --# assert
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    28
              --#  (for all i2 in Integer range 0 .. i-1 =>
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    29
              --#     (L(i2) = Liseq_ends_at(A, i2))) and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    30
              --#  L(pmax) = maxi and L(pmax) = Liseq_prfx(A, I) and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    31
              --#  0 <= i and i <= L'Last and 0 <= pmax and pmax < i and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    32
              --#  0 <= j and j <= i and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    33
              --#  maxj = Max_ext (A, i, j) and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    34
              --#  A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    35
            loop
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    36
               if (A(j) <= A(i) and
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    37
                     maxj < L(j)) then
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    38
                  maxj := L(j);
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    39
               end if;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    40
               j := j+1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    41
            end loop;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    42
            L(i) := maxj+1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    43
            if L(i) > maxi then
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    44
               maxi := maxi+1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    45
               pmax := i;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    46
            end if;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    47
         else
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    48
            maxi := maxi+1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    49
            L(i) := maxi;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    50
            pmax := i;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    51
         end if;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    52
         i := i+1;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    53
      end loop;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    54
   end Liseq_length;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    55
end Liseq;