Quelle fseqs_ops_real.pvs Sprache: PVS

fseqs_ops_real: THEORY
%------------------------------------------------------------------------
%
%  Defines some convenient operations over finite sequences of reals
%
%  EXPERIMENTAL
%
%------------------------------------------------------------------------
BEGIN

  IMPORTING  fseqs_ops[real]

  fs,gs: VAR fseq
  nefs: VAR ne_fseq
  i,n: VAR nat
  x: VAR real

  nn_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) >= 0}
  pos_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) > 0}
  neg_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) < 0}
  nz_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) /= 0}

% ------------ pointwise addition, subtraction, and multiplication

  mmin(m,n:nat): MACRO nat = IF m > n THEN n ELSE m ENDIF ;

  +(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN
                    (# length := len,
                      seq := (LAMBDA n: IF n < len THEN fs(n) + gs(n)
                                        ELSE default
                                        ENDIF)
                    #) ;

  -(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN
                    (# length := len,
                      seq := (LAMBDA n: IF n < len THEN fs(n) - gs(n)
                                        ELSE default
                                        ENDIF)
                    #) ;

  *(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN
                    (# length := len,
                      seq := (LAMBDA n: IF n < len THEN fs(n) * gs(n)
                                        ELSE default
                                        ENDIF)
                    #) ;

  nzgs: VAR nz_fseq ;

  /(fs,nzgs): fseq = LET len = mmin(l(fs),l(nzgs)) IN
                    (# length := len,
                      seq := (LAMBDA n: IF n < len THEN fs(n) / nzgs(n)
                                        ELSE default
                                        ENDIF)
                    #) ;

END fseqs_ops_real

quality71%

¤ 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:

sprechenden Kalenders