Quelle top_sigma.pvs Sprache: PVS

top_sigma: THEORY
%------------------------------------------------------------------------------
% The sigma theory introduces and defines properties of the sigma
% function that sum an arbitrary function F: [T -> real] over a range
% from low to high
%
%                             high
%                             ----
%      sigma(low, high, F) =  \     F(j)
%                             /
%                             ----
%                            j = low
%
% and alternate (tail recursion) form
%
%                                       high
%                                       ----
%      sum_it(low, high, F, a )=  a  +  \     F(j)
%                                       /
%                                       ----
%                                       j = low
%
%
%
%      by Ricky W. Butler      NASA Langley
%         Cesar Munoz          Langley ICASE
%         Paul Miner           NASA Langley
%

%      Version 1.0    original version 7/12/96
%      Version 2.0    4/2/01
%
%
%  NOTE:  T can be any subtype of the integers that is connected.  For
%         example "subrange(-12,7)", nat, or posnat.
%
%  NOTE:  Summations over functions with an arbirary number of arguments
%         is accomodated by the following technique:
%
%              G(x,y,z: real,n: nat): real
%
%              IMPORTING sigma[nat]    % or sigma_nat
%
%              sum = sigma(low,high, (LAMBDA (n:nat): G(x,y,z,n))
%
%  NOTE: The old library "sigma_real" is now subsumed by sigma_nat.
%
%  NOTE: "sigma_real.sigma_mult"  is named "sigma_scal" in "sigma"
%------------------------------------------------------------------------------

BEGIN

  IMPORTING sigma,           % generic theory
            sigma_nat,       % sigma over functions [nat --> real]
            sigma_posnat,    % sigma over functions [posnat --> real]
            sigma_int,       % sigma over functions [int --> real]
            sigma_upto,      % sigma over functions [upto[N] --> real]
            sigma_below,     % sigma over functions [below[N] --> real]
            sigma_below_sub, % equality of sigmas with different domains

            sigma_fseq_def,  % summation over finite sequences
            sigma_fseq       % Bug prevents typecheck

%  The more specific theories have stronger theorems than the generic one

%% -------  Following Obsolete

%             old_sigma_below,
%             old_sigma_below_sub,
%             old_sigma_int,
%             old_sigma_nat,
%             old_sigma_posnat,
%             old_sigma,
%             old_sigma_real,
%             old_sigma_upto


END top_sigma

quality100%

¤ Dauer der Verarbeitung: 0.11 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:

Die farbliche Syntaxdarstellung ist noch experimentell.