Quelle  trackAngles_scaf.pvs

trackAngles_scaf: THEORY
%------------------------------------------------------------------------------
%
%    Provides:
%        vfrom(a): Vect2   returns a unit vector given a real number
%        vfrom(a,k): Vect2 returns a vector given an track and a magnitude
%
%    Author:
%        Rick Butler            NASA Ltracky Research Center
%
%    EXPERIMENTAL
%
%------------------------------------------------------------------------------
BEGIN

   IMPORTING vectors_2D, 
             reals@abs_lems, 
             trig@trig_values,
             trig@trig_inverses,
             trig@atan2, angles_2D_scaf

   Track: NONEMPTY_TYPE = nnreal_lt_2pi

   a,b,c : VAR real
   alpha : VAR Track
   k     : VAR posreal
   v     : VAR Vect2
   u     : VAR Nz_vect2


   track_exists_x: LEMMA  (EXISTS (a: real): u`x = norm(u) * sin(a) AND
                                             u`y = norm(u) * cos(a))

   track_exists  : LEMMA  (EXISTS (alpha: Track): 
                              u`x = norm(u) * sin(alpha) AND
                              u`y = norm(u) * cos(alpha))




END trackAngles_scaf