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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: exp_approx.pvs   Sprache: Unknown

exp_approx: THEORY
%-----------------------------------------------------------------------------
%   Approximation of Exponential Function
%   -------------------------------------
%
%      Defines upper and lower bounds on exp:
%           - exp_lb(a,n) <= exp(a) <= exp_ub(a,n)
%           - e_lb(n)     <= e      <= e_ub(n)
%
%  Author: David Lester             Manchester University
%-----------------------------------------------------------------------------

  BEGIN

  IMPORTING exp_series
  IMPORTING reals@quad_minmax % For proof only

  n:  VAR nat
  pn: VAR posnat
  x:  VAR real
  nx: VAR negreal

  exp_neg_le1_ub(n,x): real = exp_estimate(x,2*n)

  exp_neg_le1_lb(n,x): real = exp_estimate(x,2*n+1)

  exp_neg_le1_bounds: LEMMA -1 <= x AND x < 0 IMPLIES
    (exp_neg_le1_lb(n,x) < exp(x) AND exp(x) < exp_neg_le1_ub(n,x))

  exp_neg_le1_ub_strict_decreasing_n: LEMMA -1 <= x AND x < 0 IMPLIES
      strict_decreasing?(LAMBDA (n:nat): exp_neg_le1_ub(n,x))

  exp_neg_le1_lb_strict_increasing_n: LEMMA -1 <= x AND x < 0 IMPLIES
      strict_increasing?(LAMBDA (n:nat): exp_neg_le1_lb(n,x))

  exp_neg_le1_lb_pos: LEMMA -1 <= x AND x < 0 IMPLIES exp_neg_le1_lb(pn,x) > 0

  exp_neg_ub(n,nx):posreal = LET pn= -floor(nx) IN exp_neg_le1_ub(n+1,nx/pn)^pn

  exp_neg_lb(n,nx):posreal = LET pn= -floor(nx) IN exp_neg_le1_lb(n+1,nx/pn)^pn

  exp_neg_bounds: LEMMA exp_neg_lb(n,nx) < exp(nx) & exp(nx) < exp_neg_ub(n,nx)

  exp_ub(x,n): posreal = IF    x < 0 THEN exp_neg_ub(n,x)
                         ELSIF x = 0 THEN 1
                                     ELSE 1/exp_neg_lb(n,-x) ENDIF

  exp_lb(x,n): posreal = IF    x < 0 THEN exp_neg_lb(n,x)
                         ELSIF x = 0 THEN 1
                                     ELSE 1/exp_neg_ub(n,-x) ENDIF

  exp_bounds: LEMMA exp_lb(x,n) <= exp(x) AND exp(x) <= exp_ub(x,n)

  e_lb(n) : posreal = exp_lb(1,n)

  e_ub(n) : posreal = exp_ub(1,n)

  e_bounds: LEMMA e_lb(n) <= e & e <= e_ub(n)

  e_LB : MACRO posreal = 2718281828/1000000000

  e_UB : MACRO posreal = 2718281829/1000000000

  e_bounds2: LEMMA e_LB < e & e < e_UB

  e_lb    : posreal = 271/100

  e_ub    : posreal = 272/100

  e_bound : JUDGEMENT e HAS_TYPE {x:posreal| e_lb < e AND e < e_ub}

  END exp_approx

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


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