Quelle  sort_array_def.pvs

%------------------------------------------------------------------------
%
%  sort_array_def: serves as a foundation for sort_array
%  -----------------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory provides a constructive definition of sort (named asort) to
%  provide a means to discharge the TCC produced in sort_array.  This 
%  theory is not intended to be directly used.
%
%------------------------------------------------------------------------
sort_array_def[N: nat, T: TYPE, <= : (total_order?[T]) ]: THEORY
BEGIN

  IMPORTING min_array_def[N,T,<=], permutations[N,T]

  A,A1,A2,A3: VAR below_array[N,T]
  x, t: VAR T
  ii,jj,n,i,j,ix: VAR below[N]


  P(A,jj): bool = (FORALL i,j: 0 <= i AND i < j AND j <= jj IMPLIES
                       A(i) <= A(j))

  Q(A,jj): bool = (FORALL i,j: 0 <= i AND i <= jj AND jj < j AND j < N
                       IMPLIES A(i) <= A(j))

  swap(A,jj): below_array =  A WITH [jj := A(Imin(A,jj,N-1)),
                       (Imin(A,jj,N-1)) := A(jj)]
   
  asort(A,jj): RECURSIVE below_array = 
                   (IF jj = 0 THEN swap(A,jj)
                    ELSE swap(asort(A,jj-1),jj) ENDIF)
                        MEASURE jj

  swap_perm    : LEMMA permutation_of?(A, swap(A,jj))

  asort_perm   : LEMMA permutation_of?(A,asort(A,jj))

  swap_P_and_Q : LEMMA P(A,j) AND Q(A,j) AND j < N-1 
                         IMPLIES P(swap(A,j+1),j+1) AND Q(swap(A,j+1),j+1)

  asort_P_and_Q: LEMMA P(asort(A,jj),jj) AND Q(asort(A,jj),jj)

END sort_array_def