products/Sources/formale Sprachen/PVS/analysis_ax/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Bille.ico   Sprache: PVS

Untersuchung PVS©
nth_derivatives[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
% The nth_derivatives theory defines the nth derivative of a function
%
% Developed  by Ricky W. Butler      NASA Langley Research Center
%               David Lester         Manchester University
% 
%      Version 1.0    last modified 10/30/00
%      Version 1.1    Generalised for an arbitrary interval: T DRL 27/10/03
%  
%------------------------------------------------------------------------------
BEGIN

   ASSUMING

%    connected_domain : ASSUMPTION
%         FORALL (x, y : T), (z : real) :
%             x <= z AND z <= y IMPLIES T_pred(z)

   IMPORTING deriv_domain_def

   deriv_domain    : ASSUMPTION deriv_domain?[T]

   not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING derivatives

   f: VAR [T -> real]
   m, n: VAR nat

   derivable_n_times?(f,n): RECURSIVE bool =
                                IF n = 0 THEN TRUE
                                ELSE
                                   derivable?(f) AND
                                   derivable_n_times?(deriv(f),n-1)
                                ENDIF MEASURE n


   derivable_n_times_lem: LEMMA derivable_n_times?(f,n) AND m <= n IMPLIES
                                   derivable_n_times?(f,m) 


   derivable_n_times_def: LEMMA derivable_n_times?(f, n+1) IMPLIES
                                  derivable_n_times?(deriv(f), n)



   nderiv_fun(n: nat): TYPE = {g: [T -> real] | derivable_n_times?(g,n)}


   nderiv(n: nat,f:nderiv_fun(n)):RECURSIVE [T -> real] = 
                 IF n = 0 THEN f
                 ELSE
                    nderiv(n-1,deriv(f))
                 ENDIF MEASURE n


   nderiv_derivable: LEMMA m <= n AND derivable_n_times?(f, 1 + n)
                             IMPLIES derivable?(nderiv(m, f))

   nderiv_derivable_aux: LEMMA derivable_n_times?(f, n+1) IMPLIES
                               nderiv(n+1,f) = deriv(nderiv(n,f))

   nderiv_derivable_eqv: LEMMA derivable_n_times?(f, 1 + n) IFF
                             derivable_n_times?(f,n) AND derivable?(nderiv(n, f))


END nth_derivatives



¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.4Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff