Quelle sort_inversions.pvs Sprache: PVS

sort_inversions[N: posnat, T: TYPE, <= : (total_order?[T]) ]: THEORY
%----------------------------------------------------------------------------
% inversions, i.e., index pairs i < j such that A(i) > A(j)
% are witnessses that array A is not sorted.
% transposition of adjacent elements A(j) > A(j+1) decrease
% the number of inversions. This is the basis of bubble sort.
%
% Author: Alfons Geser, National Institute of Aerospace, 2003
%----------------------------------------------------------------------------

BEGIN

  index_pair: TYPE = [below(N),below(N)]

  IMPORTING sort_array[N,T,<=],
            finite_sets[index_pair],
            permutation_ops[N]

  A    : VAR [below(N) -> T]
  inv  : VAR finite_set[index_pair]
  i,j,k: VAR below(N)
  x    : VAR T

  % to discharge the TCC for inversions
  finite_inversions: LEMMA
    is_finite[index_pair]({(i, j) | i < j & NOT A(i) <= A(j)})

  % the set of inversions, i.e, of index pairs (i,j) such that
  % A(i) and A(j) are not in sorted order
  inversions(A): finite_set[index_pair] =
    {(i,j) | i < j & NOT A(i) <= A(j)}

  pi: VAR permutation

  % to discharge the TCC for ap(pi,inv) below
  finite_ap: LEMMA
    is_finite[index_pair](LAMBDA (i, j): inv(pi(i), pi(j)))

  % apply a permutation pi to a set of index pairs
  ap(pi,inv): finite_set[index_pair] = LAMBDA (i,j): inv(pi(i),pi(j))

  % applying a permutation does not change the number of index pairs
  card_ap: LEMMA
    card[index_pair](ap(pi,inv)) = card[index_pair](inv)

  inversions_transpose: LEMMA
    j < N-1 & NOT A(j) <= A(j+1) =>
      inversions(A o transpose(j,j+1)) =
        ap(transpose(j,j+1),remove((j,j+1),inversions(A)))

  % main results:
  % 1) if (j,j+1) is an inversion then exchanging j with j+1 decreases
  %    the number of inversions by one
  % 2) if there are no inversions then A is sorted
  % 3) if there are inversions then there are inversions of the form (j,j+1)

  card_inversions_transpose: THEOREM
    j < N-1 & NOT A(j) <= A(j+1) =>
      card(inversions(A)) = 1 + card(inversions(A o transpose(j,j+1)))

  sorted_iff_no_inversions: THEOREM
    sorted?(A) <=> empty?(inversions(A))

  d: VAR nat

  successive_inversion_lem: LEMMA
    (EXISTS i: i < i+d & i+d < N & NOT A(i) <= A(i+d)) =>
    (EXISTS j: j < N-1 & NOT A(j) <= A(j+1))

  successive_inversion_exists: THEOREM
    NOT sorted?(A) => EXISTS j: j < N-1 & NOT A(j) <= A(j+1)

END sort_inversions

quality88%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.