Quellcode-Bibliothek sigma_fseq.pvs Sprache: PVS

sigma_fseq: THEORY
%------------------------------------------------------------------------------
% The summations theory provides properties of the sigma
% function that sums up a sequence of reals, e.g. fseq[real]
%
%              l(fs)
%            ----
%             sigma(fs) =  \     fs`seq(j)
%            /
%            ----
%           j = 0
%
%  WILL NOT TYPECHECK BECAUSE OF PVS BUG:
%
%      Error: the assertion (fully-instantiated? domtypes) failed.
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING sigma_fseq_def

  fs_nnr   : VAR fseq[nonneg_real]
  fs_npr   : VAR fseq[nonpos_real]
  fs_nat   : VAR fseq[nat]
  fs_npi   : VAR fseq[nonpos_int]
  fs_posnat: VAR fseq[posnat]

  sigma_fs_nnr  : JUDGEMENT sigma[nonneg_real](fs_nnr) HAS_TYPE nonneg_real

  sigma_fs_npr  : JUDGEMENT sigma[nonpos_real](fs_npr) HAS_TYPE nonpos_real

  sigma_fs_nat  : JUDGEMENT sigma[nat](fs_nat)         HAS_TYPE nat

  sigma_fs_npi  : JUDGEMENT sigma[nonpos_int](fs_npi)  HAS_TYPE nonpos_int


END sigma_fseq

quality100%

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

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders