products/sources/formale sprachen/PVS/lnexp/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Lisp

Original von: 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

¤ Dauer der Verarbeitung: 0.18 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




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.

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.


Bot Zugriff