products/Sources/formale Sprachen/COBOL/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: vect3_basis.pvs   Sprache: Unknown

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.0 Sekunden  (vorverarbeitet)  ]