Quelle vect3_basis.pvs Sprache: 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

quality86%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.