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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: scenarioBrokenHeart.arg   Sprache: PVS

Untersuchung PVS©

%------------------------------------------------------------------------------
% Arithmetic Operations defined on functions [T->complex]
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            14/06/09  Initial Version
%     Version 1.1            16/03/11  Additional rewrites added (DRL)
%
%------------------------------------------------------------------------------
complex_fun_ops[T:TYPE]: THEORY

BEGIN

  IMPORTING polar,
            structures@const_fun_def[T,complex]

  f,f1,f2: VAR [T->complex]
  f3,n0f:  VAR [T->nzcomplex]
  x,y:     VAR T
  a:       VAR complex
  n0a:     VAR nzcomplex
  c:       VAR real

  Re(f): [T -> real] = lambda x: Re(f(x));
  Im(f): [T -> real] = lambda x: Im(f(x));

  Re_fun_rew: LEMMA Re(f)(x) = Re(f(x))
  Im_fun_rew: LEMMA Im(f)(x) = Im(f(x))
  
  AUTO_REWRITE+ Re_fun_rew
  AUTO_REWRITE+ Im_fun_rew

  +(f1, f2) : [T -> complex] = lambda x : f1(x) + f2(x); 
  -(f1)     : [T -> complex] = lambda x : -f1(x);
  *(f1, f2) : [T -> complex] = lambda x : f1(x) * f2(x);
  *(a, f1)  : [T -> complex] = lambda x : a * f1(x);
  *(c, f1)  : [T -> complex] = lambda x : c * f1(x);
  -(f1, f2) : [T -> complex] = lambda x : f1(x) - f2(x);
  /(f1, f3) : [T -> complex] = lambda x : f1(x) / f3(x);
  /(f, n0a) : [T -> complex] = lambda x : f(x) / n0a;
  /(a, f3)  : [T -> complex] = lambda x : a / f3(x);
  /(c, f3)  : [T -> complex] = lambda x : c / f3(x);
  inv(f3)   : [T -> complex] = 1 / f3;
  sq(f)     : [T -> complex] = lambda x: sq(f(x));

  diff_function    : LEMMA f1 - f2 = f1 + (- f2)
  div_function     : LEMMA f1 / f3 = f1 * (1 /f3)
  scal_function    : LEMMA a * f1 = const_fun(a) * f1
  scaldiv_function : LEMMA a / f3 = const_fun(a) / f3
  negneg_function  : LEMMA - (- f1) = f1
  prod_def         : LEMMA *(f1,f2)   = (1/4)*(sq(f1+f2)-sq(f1-f2))

  conjugate(f): [T -> complex] = lambda x: conjugate(f(x));

  IMPORTING reals@real_fun_ops_aux[T]

  Re_fun_conjugate: LEMMA Re(conjugate(f)) = Re(f)
  Im_fun_conjugate: LEMMA Im(conjugate(f)) = -Im(f)

  AUTO_REWRITE+ Re_fun_conjugate
  AUTO_REWRITE+ Im_fun_conjugate

  sq_abs(f): [T -> nnreal]     = sq(Re(f)) + sq(Im(f))
  nz_fun_sq_abs_pos:  JUDGEMENT sq_abs(n0f) HAS_TYPE [T->posreal]

;
  abs(f1)   : [T->nonneg_real] = lambda x : abs(f1(x));
  complex_abs_nzfunction_pos: JUDGEMENT abs(n0f) HAS_TYPE [T->posreal]

  complex_abs_neg: LEMMA abs(-f) = abs(f)
  complex_abs_mul: LEMMA abs(f1*f2) = abs(f1)*abs(f2)

  Re_fun_add1: LEMMA Re(f1+f2) = Re(f1)+Re(f2)

  Re_fun_neg1: LEMMA Re(-f)    = -Re(f)

  Re_fun_sub1: LEMMA Re(f1-f2) = Re(f1)-Re(f2)

  Re_fun_mul1: LEMMA Re(f1*f2) = Re(f1)*Re(f2) - Im(f1)*Im(f2)
  Re_fun_mul2: LEMMA Re(a*f)   = Re(a)*Re(f) - Im(a)*Im(f)

  Re_fun_div1: LEMMA Re(f/n0f) = (Re(f)*Re(n0f) + Im(f)*Im(n0f))/sq_abs(n0f)
  Re_fun_div2: LEMMA Re(a/n0f) = (Re(a)*Re(n0f) + Im(a)*Im(n0f))/sq_abs(n0f)
  Re_fun_div3: LEMMA Re(f/n0a) = (Re(n0a)/sq_abs(n0a))*Re(f) +
                                 (Im(n0a)/sq_abs(n0a))*Im(f)

  Im_fun_add1: LEMMA Im(f1+f2) = Im(f1)+Im(f2)

  Im_fun_neg1: LEMMA Im(-f)    = -Im(f)

  Im_fun_sub1: LEMMA Im(f1-f2) = Im(f1)-Im(f2)

  Im_fun_mul1: LEMMA Im(f1*f2) = Im(f1)*Re(f2) + Re(f1)*Im(f2)
  Im_fun_mul2: LEMMA Im(a*f)   = Im(a)*Re(f) + Re(a)*Im(f)

  Im_fun_div1: LEMMA Im(f/n0f) = (Im(f)*Re(n0f) - Re(f)*Im(n0f))/sq_abs(n0f)
  Im_fun_div2: LEMMA Im(a/n0f) = (Im(a)*Re(n0f) - Re(a)*Im(n0f))/sq_abs(n0f)
  Im_fun_div3: LEMMA Im(f/n0a) = (Re(n0a)/sq_abs(n0a))*Im(f) -
                                 (Im(n0a)/sq_abs(n0a))*Re(f)

  AUTO_REWRITE+ complex_abs_neg
  AUTO_REWRITE+ complex_abs_mul
  AUTO_REWRITE+ Re_fun_add1
  AUTO_REWRITE+ Re_fun_neg1
  AUTO_REWRITE+ Re_fun_sub1
  AUTO_REWRITE+ Re_fun_mul1
  AUTO_REWRITE+ Re_fun_mul2
  AUTO_REWRITE+ Re_fun_div1
  AUTO_REWRITE+ Re_fun_div2
  AUTO_REWRITE+ Re_fun_div3
  AUTO_REWRITE+ Im_fun_add1
  AUTO_REWRITE+ Im_fun_neg1
  AUTO_REWRITE+ Im_fun_sub1
  AUTO_REWRITE+ Im_fun_mul1
  AUTO_REWRITE+ Im_fun_mul2
  AUTO_REWRITE+ Im_fun_div1
  AUTO_REWRITE+ Im_fun_div2
  AUTO_REWRITE+ Im_fun_div3
;
  =(f1,f2): bool = Re(f1) = Re(f2) AND Im(f1) = Im(f2);
  /=(f1,f2):bool = NOT (f1 = f2);
 
  c_fun_eq1: LEMMA f1  = f2 <=> Re(f1) = Re(f2) AND Im(f1) = Im(f2)
  c_fun_ne1: LEMMA f1 /= f2 <=> NOT (f1 = f2)

  AUTO_REWRITE+ c_fun_eq1
  AUTO_REWRITE+ c_fun_ne1


END complex_fun_ops

¤ 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