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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: convex_function_props.pvs   Sprache: PVS

Untersuchung PVS©

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Definition and properties of      %
%  convergent sequences of reals     %
%  -> limit of a sequence,           %
%  -> point of accumulation          %
%  -> cauchy criterion      %
%  -> Bolzano-Weierstrass theorem    %
%  -> completeness of the reals      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

convergence_sequences : THEORY

  BEGIN

  IMPORTING sequence_props, reals@abs_lems,  monotone_subsequence

  u, u1, u2 : VAR sequence[real]

  l, l1, l2 : VAR real

  a, b, c, x : VAR real

  epsilon : VAR posreal

  i, j, n, m : VAR nat


  %--------------------
  %  Convergence to l
  %--------------------

  convergence(u, l) : bool =
 FORALL epsilon : EXISTS n :
     FORALL i : i >= n IMPLIES abs(u(i) - l) < epsilon

  %-------------------------
  %  Point of accumulation
  %-------------------------

  accumulation(u, a) : bool =
 FORALL epsilon, n : EXISTS i : i >= n AND abs(u(i) - a) < epsilon

  %--------------------
  %  Cauchy sequence
  %--------------------

  cauchy(u) : bool =
 FORALL epsilon : EXISTS n :
     FORALL i, j : i >= n AND j >= n IMPLIES abs(u(i) - u(j)) < epsilon






  %-----------------------
  %  The limit is unique  
  %-----------------------

  unique_limit : LEMMA
 convergence(u, l1) AND convergence(u, l2) IMPLIES l1 = l2



  %---------------------------------
  %  Limit of convergent sequences
  %---------------------------------

  convergent?(u) : bool = EXISTS l : convergence(u, l)

  convergent_seq?(u): MACRO bool = convergent?(u)

  v : VAR (convergent?)

  limit(v) : real = epsilon(LAMBDA l : convergence(v, l))

  limit_lemma : LEMMA convergence(v, limit(v))

  limit_def : LEMMA  limit(v) = l IFF convergence(v, l)



  %--------------------------------------------------------
  %  A subsequence of a convergent sequence is convergent
  %--------------------------------------------------------

  convergence_subsequence : LEMMA
 convergence(u1, l) AND subseq(u2, u1) IMPLIES convergence(u2, l)

  

  %----------------------------------------
  %  The limit is a point of accumulation
  %----------------------------------------

  limit_accumulation : LEMMA 
 convergence(u, l) IMPLIES accumulation(u, l)



  %------------------------------------------------------------------
  %  a is a point of accumulation iff a sub-sequence converges to a
  %------------------------------------------------------------------

  %--- extraction ---%

  g(u, a)(n) : RECURSIVE nat =
 IF n = 0 THEN 0
 ELSE  epsilon! i : g(u, a)(n - 1) < i AND abs(u(i) - a) < 1/n
 ENDIF
      MEASURE n


  %--- property of g when a is an accumulation point of a ---%

  g_prop : LEMMA accumulation(u, a) IMPLIES
 FORALL n : g(u, a)(n) < g(u, a)(n+1) AND abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1)

  g_increasing : COROLLARY
 accumulation(u, a) IMPLIES strict_increasing?(g(u, a))

  g_convergence : COROLLARY
 accumulation(u, a) IMPLIES FORALL n : abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1)


  %--- main theorem ---%

  accumulation_subsequence : THEOREM
 accumulation(u, a) IFF EXISTS u1 : subseq(u1, u) AND convergence(u1, a)



  %-------------------------------------------------------------
  %  a point of accumulation of a Cauchy sequence is its limit
  %-------------------------------------------------------------

  cauchy_accumulation : THEOREM
 cauchy(u) AND accumulation(u, a) IMPLIES convergence(u, a)

  cauchy_subsequence : COROLLARY
 cauchy(u) AND subseq(u1, u) AND convergence(u1, l)
     IMPLIES convergence(u, l)




  %----------------------------------------------
  %  Monotone, bounded sequences are convergent 
  %----------------------------------------------

  v1 : VAR { u | bounded_above?(u) }

  v2 : VAR { u | bounded_below?(u) }

  increasing_bounded_convergence : LEMMA
 increasing?(v1) IMPLIES convergence(v1, sup(v1))

  decreasing_bounded_convergence : LEMMA
 decreasing(v2) IMPLIES convergence(v2, inf(v2))




  %--------------------------------------------------
  %  Bolzano-Weierstrass theorem:
  %  a bounded sequence has a point of accumulation
  %--------------------------------------------------

  %--- bounded sequence ---%

  w : VAR { u | bounded_above?(u) AND bounded_below?(u) }  

  
  %--- Bolzano/Weirstrass theorem ---%

  bolzano_weierstrass1 : COROLLARY
 EXISTS a : inf(w) <= a AND a <= sup(w) AND accumulation(w, a)

  bolzano_weierstrass2 : COROLLARY  EXISTS a : accumulation(w, a)

  bolzano_weierstrass3 : COROLLARY
 EXISTS u : subseq(u, w) AND convergent?(u)

  bolzano_weierstrass4 : COROLLARY
 (FORALL i : a <= u(i) AND u(i) <= b) IMPLIES
     (EXISTS c : a <= c AND c <= b AND accumulation(u, c))




  %--------------------------------
  %  A Cauchy sequence is bounded
  %--------------------------------

  prefix_bounded1 : LEMMA
 EXISTS a : FORALL i : i <= n IMPLIES u(i) <= a

  prefix_bounded2 : LEMMA
 EXISTS a : FORALL i : i <= n IMPLIES a <= u(i)

  cauchy_bounded : LEMMA
 cauchy(u) IMPLIES bounded_above?(u) AND bounded_below?(u)




  %--------------------------------------------------
  %  Completeness : a Cauchy sequence is convergent
  %--------------------------------------------------

  convergence_cauchy1 : LEMMA convergent?(u) IMPLIES cauchy(u)

  convergence_cauchy2 : LEMMA cauchy(u) IMPLIES convergent?(u)

  convergence_cauchy : THEOREM  convergent?(u) IFF cauchy(u)

  END convergence_sequences


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.3Angebot  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