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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: power_series_deriv_scaf.pvs   Sprache: PVS

Untersuchung PVS©

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  General convergence of functions [T -> real]  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

convergence_functions [T : TYPE FROM real] : THEORY
BEGIN

  IMPORTING reals@real_fun_ops, epsilon_lemmas

  epsilon, delta : VAR posreal
  e, e1, e2 : VAR posreal
  E, E1, E2 : VAR setof[real]
  f, f1, f2 : VAR [T -> real]
  g : VAR [T -> nzreal]
  l, l1, l2, a, b, z : VAR real
  x, y : VAR T

  %---------------------------
  %  Reals adherent to a set
  %---------------------------

  adh(E) : setof[real] =
 { z | FORALL e : EXISTS x : E(x) AND abs(x - z) < e }


  member_adherent : LEMMA   E(x) IMPLIES adh(E)(x)

  adherence_subset1 : LEMMA
 subset?(E1, E2) AND adh(E1)(z) IMPLIES adh(E2)(z)

  adherence_subset2 : LEMMA
 subset?(E1, E2) IMPLIES subset?(adh(E1), adh(E2))


  adherence_prop1 : LEMMA
 FORALL e, E, (a : (adh(E))) :
     EXISTS x : E(x) AND abs(x - a) < e

  adherence_prop2 : LEMMA 
 FORALL e1, e2, E, (a : (adh(E))) :
     EXISTS x : E(x) AND abs(x - a) < e1 AND abs(x - a) < e2



  %------------------------------------------------------
  %  Definition of convergence and immediate properties
  %------------------------------------------------------

  convergence(f, E, a, l) : bool = 
 adh(E)(a) AND 
 FORALL epsilon : EXISTS delta : 
     FORALL x : E(x) AND abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon

  convergence_unicity : LEMMA
 FORALL E, f, a, l1, l2 : 
     convergence(f, E, a, l1) AND convergence(f, E, a, l2)
        IMPLIES l1 = l2

  subset_convergence : LEMMA
 subset?(E1, E2) IMPLIES
     FORALL f, (a : (adh(E1))), l :
         convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l)

  subset_convergence2 : LEMMA
 FORALL E1, E2, f, (a : (adh(E1))), l :
     subset?(E1, E2) AND convergence(f, E2, a, l)
   IMPLIES convergence(f, E1, a, l)

  convergence_in_domain : LEMMA
 FORALL f, x, l : E(x) AND convergence(f, E, x, l) IMPLIES l = f(x)




  %----------------------------------
  %  Limits and function operations
  %----------------------------------

  convergence_sum : LEMMA
 FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1) 
     AND convergence(f2, E, a, l2)
        IMPLIES convergence(f1 + f2, E, a, l1 + l2)


  convergence_neg : LEMMA
 FORALL E, f1, a, l1 :
  convergence(f1, E, a, l1) 
        IMPLIES convergence(- f1, E, a, - l1)


  convergence_diff : LEMMA
 FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1) 
     AND convergence(f2, E, a, l2)
        IMPLIES convergence(f1 - f2, E, a, l1 - l2)


  convergence_prod : LEMMA
 FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1) 
     AND convergence(f2, E, a, l2)
        IMPLIES convergence(f1 * f2, E, a, l1 * l2)


  convergence_const : LEMMA
 FORALL E, (a : (adh(E))), b : convergence(const_fun(b), E, a, b)


  convergence_scal : LEMMA
 FORALL E, f1, a, l1, b :
  convergence(f1, E, a, l1)
 IMPLIES convergence(b * f1, E, a, b * l1)


  convergence_inv : LEMMA
 FORALL E, g, a, l1:
  convergence(g, E, a, l1)
     AND l1 /= 0
 IMPLIES convergence(1/g, E, a, 1/l1)


  convergence_div : LEMMA
 FORALL E, f, g, a, l1, l2 :
  convergence(f, E, a, l1)
     AND convergence(g, E, a, l2)
     AND l2 /= 0
 IMPLIES convergence(f/g, E, a, l1/l2)
 


  %---------------------
  %  Identity function
  %---------------------

  convergence_identity : LEMMA 
 FORALL E, (a : (adh(E))) : convergence(I[T], E, a, a)



  %-----------------------------
  %  Limit preserve order
  %-----------------------------

  convergence_order : LEMMA
 FORALL E, f1, f2, a, l1, l2 :
  convergence(f1, E, a, l1)
     AND convergence(f2, E, a, l2)
     AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x))
 IMPLIES l1 <= l2
  

  %-------------------------------------------
  %  Bounds on function are bounds on limits
  %-------------------------------------------

  convergence_lower_bound : COROLLARY
 FORALL E, f, b, a, l :
  convergence(f, E, a, l)
     AND (FORALL x : E(x) IMPLIES b <= f(x))
 IMPLIES b <= l

  convergence_upper_bound : COROLLARY
 FORALL E, f, b, a, l :
  convergence(f, E, a, l)
     AND (FORALL x : E(x) IMPLIES f(x) <= b)
 IMPLIES l <= b


  %--------------------------
  %  Function constant on E
  %--------------------------

  convergence_locally_constant : LEMMA
 FORALL E, f, b, (a : (adh(E))) :
     (FORALL x : E(x) IMPLIES f(x) = b)
 IMPLIES convergence(f, E, a, b)
  

  %-------------
  %  Squeezing
  %-------------

  convergence_squeezing : LEMMA
 FORALL f1, f2, f, a, l :
     convergence(f1, E, a, l) AND convergence(f2, E, a, l)
 AND (FORALL x : E(x) IMPLIES f1(x) <= f(x) AND f(x) <= f2(x))
    IMPLIES
     convergence(f, E, a, l)


END convergence_functions

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





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

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

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