Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vect3_basis.pvs Sprache: PVS

Original von: PVS^©

vect3_basis: THEORY
%----------------------------------------------------------------------------
% Given one vector of norm 1, this gives an orthonormal basis containing that vector
%
%----------------------------------------------------------------------------
BEGIN

    IMPORTING perpendicular_3D, cross_3D

    t,tp: VAR real
    P0,Q,v,w,u,c,d,x,y,del: VAR Vect3
    nzv,nzw,nzu: VAR Nz_vect3
    R : VAR posreal % Radius of the sphere to be rotated and planed

   vect3_orthog_tox(v): Vect3 = v

   vect3_orthog_toy(v): Vect3 =
      IF v`x/=0 OR v`y /=0 THEN (v`y,-v`x,0)
      ELSE (1,0,0) ENDIF

   vect3_orthog_toy_def: LEMMA v/=zero IMPLIES orthogonal?(v,vect3_orthog_toy(v))

   vect3_orthog_toz(v): Vect3 = cross(v,vect3_orthog_toy(v))

   vect3_orthog_toz_def: LEMMA orthogonal?(v,vect3_orthog_toz(v))
             AND
          orthogonal?(vect3_orthog_toy(v),vect3_orthog_toz(v))

   %%%%%%% The normalized basis %%%%%%%

   vect3_orthonorm_tox(nzv): Normalized = ^(nzv)

   vect3_orthonorm_toy(nzv): Normalized = ^(vect3_orthog_toy(nzv))

   vect3_orthonorm_toz(nzv): Normalized = ^(vect3_orthog_toz(nzv))

   vect3_orthonorm_basis: LEMMA
     LET v = vect3_orthonorm_tox(nzv),
         u = vect3_orthonorm_toy(nzv),
  w = vect3_orthonorm_toz(nzv)
     IN
         orthogonal?(v,u) AND orthogonal?(u,w) AND orthogonal?(w,v)

  %%%%%%% Rotation to Equator %%%%%%%

  %%%%%%% A distance preserving map... %%%%%%%

  Equator_map(nzv)(w): Vect3 =
    LET xmult: Vect3 = vect3_orthonorm_tox(nzv),
        ymult: Vect3 = vect3_orthonorm_toy(nzv),
zmult: Vect3 = vect3_orthonorm_toz(nzv)
    IN
        (xmult*w,ymult*w,zmult*w)

  Equator_map_def: LEMMA normalized?(nzv) IMPLIES
    Equator_map(nzv)(nzv) = (1,0,0)

  transpose_Equator_map(nzv): [Vect3,Vect3,Vect3] =
    LET xvect: Vect3 = vect3_orthonorm_tox(nzv),
        yvect: Vect3 = vect3_orthonorm_toy(nzv),
zvect: Vect3 = vect3_orthonorm_toz(nzv),
xmultinv: Vect3 = (xvect`x,yvect`x,zvect`x),
ymultinv: Vect3 = (xvect`y,yvect`y,zvect`y),
zmultinv: Vect3 = (xvect`z,yvect`z,zvect`z)
    IN  (xmultinv,ymultinv,zmultinv)

  Equator_map_inv(nzv)(w): Vect3 =
    LET xvect: Vect3 = vect3_orthonorm_tox(nzv),
        yvect: Vect3 = vect3_orthonorm_toy(nzv),
zvect: Vect3 = vect3_orthonorm_toz(nzv),
xmultinv: Vect3 = (xvect`x,yvect`x,zvect`x),
ymultinv: Vect3 = (xvect`y,yvect`y,zvect`y),
zmultinv: Vect3 = (xvect`z,yvect`z,zvect`z)
    IN
        (xmultinv*w,ymultinv*w,zmultinv*w)

  Equator_map_inv_def: LEMMA
    Equator_map(nzv)(Equator_map_inv(nzv)(w)) = w

  %%%%%%% Translating to 2D Plane %%%%%%%

  sphere_to_2D_plane(nzv)(w): Vect2 =
    LET xmult: Vect3 = vect3_orthonorm_tox(nzv),
        ymult: Vect3 = vect3_orthonorm_toy(nzv),
zmult: Vect3 = vect3_orthonorm_toz(nzv)
    IN
        (ymult*w,zmult*w)

END vect3_basis

¤ Dauer der Verarbeitung: 0.15 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.