Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: globnames.mli Sprache: PVS

Original von: PVS^©

angles_2D: THEORY
%------------------------------------------------------------------------------
%
%    Provides:
%        vfrom(a): Vect2   returns a unit vector given an angle
%        vfrom(a,k): Vect2 returns a vector given an angle and a magnitude
%
%        angle(u): nnreal_lt_2pi returns an angle between 0,2*pi given a vector
%        Angle(u): nnreal_lt_2pi returns an angle between 0,2*pi given a vector
%                                    (defined used atan2)
%        See angle_Angle which proves equivalence
%
%    Author:
%        Rick Butler            NASA Langley Research Center
%
%    EXPERIMENTAL
%
%------------------------------------------------------------------------------
BEGIN

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

   Angle: NONEMPTY_TYPE = nnreal_lt_2pi

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

%  -------- Vector from an angle -------------

   v_from(a: real): Vect2 = (# x := cos(a), y := sin(a) #)

   v_from(a: real, k: posreal): Vect2 = (# x := k*cos(a), y := k*sin(a) #)

   v_from_k_1: LEMMA v_from(a,1) = v_from(a)

   norm_v_from: LEMMA norm(v_from(a,k)) = k

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

%  -------- Angle from a vector -------------

   vec_from(a: Angle, k: posreal): MACRO Vect2 = v_from(a,k)

   norm_vec_from : LEMMA norm(vec_from(alpha,k)) = k

   vec_from_inj  : LEMMA injective?(vec_from)

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

   angle(u: Nz_vect2): {alpha: Angle | u = vec_from(alpha, norm(u))}
                       = choose({alpha: Angle | u = vec_from(alpha, norm(u))})

   vec_from_angle   : LEMMA vec_from(angle(u),norm(u)) = u

   angle_vec_from : LEMMA angle(vec_from(alpha,k)) = alpha

   Angle(u: Nz_vect2): Angle = atan2(u`x,u`y)

   angle_Angle: LEMMA angle(u) = Angle(u)

   vec_from_Angle: LEMMA vec_from(Angle(u), norm(u)) = u

%  -------- Special Values -----------

   x: VAR posreal
   angle_x0: LEMMA angle(mk_vect2(x,0)) = 0
   angle_0x: LEMMA angle(mk_vect2(0,x)) = pi/2
   angle_xx: LEMMA angle(mk_vect2(x,x)) = pi/4

   ngr: VAR negreal
   angle_n0: LEMMA angle(mk_vect2(ngr,0)) = pi
   angle_0n: LEMMA angle(mk_vect2(0,ngr)) = 3*pi/2

   angle_nx: LEMMA angle(mk_vect2(-x,x)) = 3*pi/4
   angle_xn: LEMMA angle(mk_vect2(x,-x)) = 7*pi/4
   angle_nn: LEMMA angle(mk_vect2(-x,-x)) = 5*pi/4

%  --------- Properties ------------------

   vfrom_sub          : LEMMA v_from(a-b) = (cos(a-b),sin(a-b))

   v_from_dot         : LEMMA v_from(a)*v_from(b) = cos(a-b)

   ka,kb: VAR posreal
   v_from_dot_k       : LEMMA v_from(a,ka)*v_from(b,kb) = ka*kb*cos(a-b)

   dot_prod_angles    : LEMMA LET s = v_from(c),
                                  nv = v_from(a),
                                  v = v_from(b) IN
                             s*(nv-v) = cos(a-c) - cos(b-c)

END angles_2D

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.