Quellcode-Bibliothek concat_arrays.pvs Sprache: PVS

concat_arrays [n:nat, m:nat, T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory defines the concatenation operator o for arrays
%
%------------------------------------------------------------------------

BEGIN

  IMPORTING below_arrays

  a_n: VAR below_array[n,T]
  a_m: VAR below_array[m,T]
  nm : VAR below(n+m)

  o(a_n, a_m): below_array[n+m,T] = (LAMBDA nm: IF nm < n THEN a_n(nm)
                                                 ELSE a_m(nm - n)
                                                 ENDIF)

  i: VAR below(n)
  j: VAR {i: int | i >= n AND i < n+m}

  concat_array_bot0: THEOREM m = 0 IMPLIES a_n o a_m = a_n

  concat_array_top0: THEOREM n = 0 IMPLIES a_n o a_m = a_m

  concat_array_bot : THEOREM (a_n o a_m)(i) = a_n(i)

  concat_array_top : THEOREM (a_n o a_m)(j) = a_m(j-n)

END concat_arrays

quality99%

¤ 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.4Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.