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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: partial_function_props.prf   Sprache: PVS

Untersuchung PVS©

riesz_interval_funs[a:real,b: {bb:real | a < bb}]: THEORY
%------------------------------------------------------------------------------
%  Real valued functions on a closed interval
%------------------------------------------------------------------------------

BEGIN

   IMPORTING real_metric_space,real_fun_on_compact_sets,
         metric_space_real_fun


   c: VAR real
   M: VAR nnreal

   Intab : set[real] = closed_intv(a,b)
   INTab : TYPE = (closed_intv(a,b))

   h,f,g: VAR [INTab -> real]

   x :VAR INTab

   IMPORTING metric_space_real_fun[INTab,real_dist]

   bounded_on_int?(h): bool = EXISTS (M:nnreal): FORALL (x): abs(h(x))<=M

   bounded_on_int_sum_closed: LEMMA bounded_on_int?(f) AND bounded_on_int?(h) IMPLIES bounded_on_int?(f+h)

   bounded_on_int_const_closed: LEMMA bounded_on_int?(f) IMPLIES bounded_on_int?(c*f)

   fun_norm(f: (bounded_on_int?)): {M:nnreal | (FORALL (x): abs(f(x))<=M) AND (FORALL (M1:real): M1 < M IMPLIES 
           EXISTS (x): abs(f(x)) > M1)}

   fun_norm_dist(f,g:(bounded_on_int?)): {k:nnreal|k=0 IFF f=g} = fun_norm(f-g)

   fun_norm_bound: LEMMA FORALL (f:(bounded_on_int?),x): abs(f(x)) <= fun_norm(f)

   fun_norm_zero: LEMMA bounded_on_int?(f) IMPLIES (fun_norm(f) = 0 IFF f = (LAMBDA (y:INTab): 0))

   fun_norm_scal: LEMMA FORALL (f:(bounded_on_int?),c): fun_norm(c*f) = abs(c)*fun_norm(f)

   fun_norm_triangle: LEMMA FORALL (f,g:(bounded_on_int?)): fun_norm(f+g) <= fun_norm(f)+fun_norm(g)

   bounded_funs_metric_space: LEMMA metric_space?[(bounded_on_int?),fun_norm_dist](bounded_on_int?)



   int_compact: LEMMA compact?(Intab)

   Bounded_Function : TYPE = (bounded_on_int?)

   continuous_on_int?(h): bool = continuous?(h,Intab)

   Continuous_Function: TYPE = (continuous_on_int?)

   fc,gc : VAR Continuous_Function
   fb,gb: VAR Bounded_Function

   continuous_implies_bounded: LEMMA FORALL (h:Continuous_Function): bounded_on_int?(h)

   continuous_function_bounded: JUDGEMENT Continuous_Function Subtype_of Bounded_Function




END riesz_interval_funs


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