Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: partitions_scaf.prf   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.28Angebot  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



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik