| products/Sources/formale Sprachen/PVS/structures/ (KI Agentensystem Version 22©) Datei vom 28.9.2014 mit Größe 1 kB |
|
SSL max_array_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------
% % max_array_def: foundation for max_array % --------------------------------------- % % Author: Ricky W. Butler % % This theory provides a constructive definition of max (named Imax) to % provide a means to discharge the TCC produced in max_array. This % theory is not intended to be directly used. % %------------------------------------------------------------------------ max_array_def[N: nat, T: TYPE, <= : (total_order?[T]) ]: THEORY BEGIN A,A1,A2: VAR ARRAY[below(N) -> T] t, t1, t2: VAR T ii,jj,j: VAR below(N) amax(A,ii,jj): below(N) = IF A(ii) <= A(jj) THEN jj ELSE ii ENDIF imax_rec(A,ii,jj): RECURSIVE below(N) = IF jj <= ii THEN ii ELSE amax(A,jj,imax_rec(A,ii,jj-1)) ENDIF MEASURE (LAMBDA A,ii,jj: jj) imax_rec_lem: LEMMA ii <= j AND j <= jj IMPLIES A(j) <= A(imax_rec(A,ii,jj)) imax_rec_rng: LEMMA ii <= jj IMPLIES ii <= imax_rec(A,ii,jj) AND imax_rec(A,ii,jj) <= jj abv(ii): TYPE = {i: nat | ii <= i AND i < N} Imax_rec(A,ii,(jj: abv(ii))): subrange(ii,jj) = imax_rec(A,ii,jj) Imax(A,ii,(jj: abv(ii))): {i: subrange(ii,jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(j) <= A(i))} Imax_1: LEMMA Imax(A,ii,ii) = ii END max_array_def ¤ 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.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28