| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle sort_array_def.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28