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 trackAngles_2D.pvs Sprache: PVS

trackAngles_2D: THEORY
%------------------------------------------------------------------------------
%
%    Provides:
%        vec_from(a,k): Vect2 returns a vector given an track and a magnitude
%
%        track(u): Track returns an track angle between 0,2*pi given a vector
%                                    (defined used atan2)
%
%        trk(u): atan2(u`y,u`x) is equivalent
%
%    Author:
%        Rick Butler            NASA Langley Research Center
%
%    EXPERIMENTAL
%
%------------------------------------------------------------------------------
BEGIN

   IMPORTING trackAngles_scaf

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

%  -------- Vector from an track angle 0 to 2 PI

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

   vec_from(a: Track, k: posreal): Vect2 = v_from(a,k)

   trk(u: Nz_vect2)  : Track = atan2(u`y,u`x)

%%   sqrt_scal      : LEMMA FORALL (x: nnreal): abs(a)*sqrt(x) = sqrt(sq(a)*x)

   track(u: Nz_vect2): {alpha: Track | u = vec_from(alpha, norm(u))}

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

   vec_from_nz    : LEMMA vec_from(alpha,k) /= zero

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

   vec_from_inj   : LEMMA injective?(vec_from)

   vec_from_track : LEMMA vec_from(track(u),norm(u)) = u

   track_vec_from : LEMMA track(vec_from(alpha,k)) = alpha

   track_trk      : LEMMA track(u) = trk(u)

   vec_from_trk   : LEMMA vec_from(trk(u), norm(u)) = u

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

   x: VAR posreal
   track_x0: LEMMA track(mk_vect2(x,0)) = pi/2
   track_0x: LEMMA track(mk_vect2(0,x)) = 0
   track_xx: LEMMA track(mk_vect2(x,x)) = pi/4

   ngr: VAR negreal
   track_n0: LEMMA track(mk_vect2(ngr,0)) = 3*pi/2
   track_0n: LEMMA track(mk_vect2(0,ngr)) = pi

   track_nx: LEMMA track(mk_vect2(-x,x)) = 7*pi/4
   track_xn: LEMMA track(mk_vect2(x,-x)) = 3*pi/4
   track_nn: LEMMA track(mk_vect2(-x,-x)) = 5*pi/4

%  -------- Properties of v_from -------------

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

   v_from_dot         : LEMMA v_from(a,1)*v_from(b,1) = 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_tracks    : LEMMA LET s = v_from(c,1),
                                  nv = v_from(a,1),
                                  v = v_from(b,1) IN
                             s*(nv-v) = cos(a-c) - cos(b-c)

END trackAngles_2D

quality100%

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