Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

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.1 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.