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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: product_posnat.pvs   Sprache: PVS

Untersuchung PVS©

trig_basic : THEORY
%-----------------------------------------------------------------------------
%     trig_basic:
%     -----------
%         - definition of pi with crude upper and lower bounds
%         - definition of sin, cos, and tan
%         - pythagorean properties: sq(sin(a)) + sq(cos(a)) = 1 
%         - sum and difference of two angles
%         - double angle formulas
%         - negative properties, e.g. sin(-a)
%         - periodicity, e.g. sin(a) = sin(a + 2 * j * pi) 
%         - co-function identities, e.g. sin(pi/2 - a) = cos(a)
%         - location of zeros of trig functions
%
%   Version 1.1 27/10/03 Foundational Version David Lester
%
%   CHANGES 
%         - Oct 21 2004 (C. Munoz) Moved pi_lb, pi_ub, pi_bound to atan_approx
%
%-----------------------------------------------------------------------------
BEGIN

  IMPORTING reals@sqrt, sincos_def, atan_approx

  a,b,c,d           : VAR real
  nnc               : VAR nonneg_real 
  j                 : VAR integer
  
% This is now in atan_approx.pvs
%
%  pi_lb  : real = 31415926/10000000

%  pi_ub  : real = 31415927/10000000
%
%  pi_bound : JUDGEMENT pi HAS_TYPE {r:posreal | pi_lb < r AND r < pi_ub}

% -------------------- definition of sin and cos --------------------
%
% This is now in sincos_def.pvs
%
%  trig_range  : TYPE = {a | -1 <= a AND a <= 1}
%
%  sin(x:real) : real = sin_phase(x-2*pi*floor(x/(2*pi)))
%  cos(x:real) : real = cos_phase(x-2*pi*floor(x/(2*pi)))
%
%  sin_range_ax: LEMMA -1 <= sin(a) AND sin(a) <= 1
%  cos_range_ax: LEMMA -1 <= cos(a) AND cos(a) <= 1
%
%  sin_range   : JUDGEMENT sin(a) HAS_TYPE trig_range
%  cos_range   : JUDGEMENT cos(a) HAS_TYPE trig_range
%
%  Tan?(a)        : bool = cos(a) /= 0

%  tan(a:(Tan?))  : real = sin(a)/cos(a)

% -------------------- Pythagorean Property --------------------
 
  sin2_cos2    : LEMMA sq(sin(a)) + sq(cos(a)) = 1

  cos2         : LEMMA sq(cos(a)) = 1 - sq(sin(a)) 

  sin2         : LEMMA sq(sin(a)) = 1 - sq(cos(a)) 

% --------------------- Basic Values ----------------------------

  cos_0         : LEMMA cos(0) = 1 

  sin_0         : LEMMA sin(0) = 0

  sin_pi2       : LEMMA sin(pi/2) = 1

  cos_pi2       : LEMMA cos(pi/2) = 0

  tan_0         : LEMMA tan(0) = 0

% --------------------- Negative Properties ----------------------

  sin_neg : LEMMA sin(-a) = -sin(a) 
  cos_neg : LEMMA cos(-a) = cos(a) 
  tan_neg : LEMMA FORALL(a:(Tan?)): tan(-a) = -tan(a)


% -------------------- Co-Function Identities -----------------------

  cos_sin    : LEMMA cos(a) = sin(a+pi/2)
  sin_cos    : LEMMA sin(a) = -cos(a+pi/2)
  sin_shift  : LEMMA sin(pi/2 - a) = cos(a)
  cos_shift  : LEMMA cos(pi/2 - a) = sin(a)

% --------------------- Arguments involving pi ---------------------

  neg_cos     : LEMMA -cos(a) = cos(a+pi)
  neg_sin     : LEMMA -sin(a) = sin(a+pi)

  sin_pi      : LEMMA sin(pi) = 0
  cos_pi      : LEMMA cos(pi) = -1
  tan_pi      : LEMMA tan(pi) = 0
  sin_3pi2    : LEMMA sin(3*pi/2) = -1
  cos_3pi2    : LEMMA cos(3*pi/2) = 0
  sin_2pi     : LEMMA sin(2*pi) = 0
  cos_2pi     : LEMMA cos(2*pi) = 1
  tan_2pi     : LEMMA tan(2*pi) = 0

% ----------------- Sum and Difference of Two Angles ----------------

  sin_plus  : LEMMA sin(a + b) = sin(a)*cos(b) + cos(a)*sin(b)   
  sin_minus : LEMMA sin(a - b) = sin(a)*cos(b) - sin(b)*cos(a)

  cos_plus  : LEMMA cos(a + b) = cos(a)*cos(b) - sin(a)*sin(b)
  cos_minus : LEMMA cos(a - b) = cos(a)*cos(b) + sin(a)*sin(b)

  tan_plus  : LEMMA Tan?(a) AND Tan?(b) AND Tan?(a+b) AND
                    tan(a) * tan(b) /= 1 IMPLIES                 
                      tan(a + b) = (tan(a) + tan(b))/(1 - tan(a)*tan(b)) 

  tan_minus : LEMMA Tan?(a) AND Tan?(b) AND Tan?(a-b) AND
                    tan(a) * tan(b) /= -1 IMPLIES                 
                      tan(a - b) = (tan(a) - tan(b))/(1 + tan(a)*tan(b))

  arc_sin_cos  : LEMMA sq(a)+sq(b)=sq(c) IMPLIES
                            EXISTS d: a = c*cos(d) AND b = c*sin(d)

  pythagorean  : LEMMA sq(a)+sq(b)=sq(nnc) IMPLIES
                            EXISTS(alpha:real): nnc=a*cos(alpha)+b*sin(alpha)

% -------------------- Double Angle Formulas -------------------- 

   sin_2a     : LEMMA sin(2*a) = 2 * sin(a) * cos(a)
   cos_2a     : LEMMA cos(2*a) = cos(a)*cos(a) - sin(a)*sin(a)
   cos_2a_cos : LEMMA cos(2*a) = 2 * cos(a)*cos(a) - 1
   cos_2a_sin : LEMMA cos(2*a) = 1 - 2 * sin(a)*sin(a)
   tan_2a     : LEMMA Tan?(a) AND Tan?(2*a) AND 
                      tan(a) * tan(a) /= 1 IMPLIES 
                        tan(2*a) = 2 * tan(a)/(1 - tan(a) * tan(a))
 
% ------------------------- Periodicity -----------------------------

%  IMPORTING reals@prelude_aux_reals

  n: VAR nat
  k: VAR integer

  sin_period  : LEMMA sin(a) = sin(a + 2 * j * pi) 
  cos_period  : LEMMA cos(a) = cos(a + 2 * j * pi) 
  tan_period  : LEMMA Tan?(a) IMPLIES tan(a) = tan(a + j * pi) 

  sin_k_pi    : LEMMA sin(k*pi) = 0
  cos_2k_pi   : LEMMA cos(2*k*pi) = 1
  cos_k_pi    : LEMMA cos(k*pi) = (-1)^(k)
  sin_k_pi2   : LEMMA sin(k*pi + pi/2) = (-1)^k 
  tan_k_pi    : LEMMA tan(k*pi) = 0

% -------------------- Characterization of zeroes -------------------


  sin_eq_0_2pi : COROLLARY 0 <= a AND a <= 2*pi IMPLIES
                    (sin(a)=0 IFF a=0 OR a=pi OR a=2*pi)

  cos_eq_0_2pi : COROLLARY 0 <= a AND a <= 2*pi IMPLIES
                    (cos(a)=0 IFF a=pi/2 OR a=3*pi/2)

  sin_eq_0     : LEMMA sin(a) = 0 IFF EXISTS (i: int): a = i * pi

  cos_eq_0     : LEMMA cos(a) = 0 IFF EXISTS (i: int): a = i * pi + pi/2


% ---------------------- Maximum Points -----------------------------
 
  sin_eq_1     : LEMMA sin(a) = 1 IFF EXISTS (i: int): a = 2 * i * pi + pi/2
  cos_eq_1     : LEMMA cos(a) = 1 IFF EXISTS (i: int): a = 2 * i * pi 

END trig_basic


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