Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: PVS

Original von: PVS^©

closest_approach_relative_2D: THEORY
%------------------------------------------------------------------------------
%
% The closest approach of approach (cpa) only depends upon the relative position and
% relative velocity between two trajectories.   Therefore it is convenient
% to cast the cpa theory in terms of relative vectors:
%
%     s = po - qo
%
%     v = v - u
%
%  Author: Ricky Butler              NASA Langley Research Center
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING closest_approach_2D

  s,v,
  so,si,
  vo,vi,
  nvo,nvi : VAR Vect2
  t,t1,t2 : VAR real
  nzv : VAR Nz_vect2

  dot_pos?(s,v): bool = s * v > 0

  dot_nneg?(s,v): bool = s * v >= 0

  divergent?(s,v): MACRO bool =
    divergent?(s,zero,v,zero)

  divergent_lem: LEMMA
      divergent?(s,v) IFF (FORALL (t: posreal): norm(s) < norm(s+t*v))

  dot_pos_comm : LEMMA
    dot_pos?(s,v) IFF dot_pos?(-s,-v)

  dot_pos_divergent : LEMMA
    dot_pos?(s,v) IMPLIES divergent?(s,v)

  sq_dist_at(s,v,t) : nnreal =
    sq_dist(s+t*v,zero)

  divergent_lt : LEMMA
    divergent?(s,v) IFF
      FORALL(t1,t2:real):
        0 <= t1 AND t1 < t2 IMPLIES
        sq_dist_at(s,v,t1) < sq_dist_at(s,v,t2)

  divergent_dot_pos: LEMMA
     divergent?(s,v) IMPLIES (dot_pos?(s,v) OR s*v = 0)

  diverg_dot_nneg : LEMMA
     divergent?(s,v) IMPLIES dot_nneg?(s,v)

  divergent_v_neq_0 : LEMMA
    divergent?(s,v) IMPLIES v /= zero

  dot_nneg_divergent_nzv: THEOREM
    dot_nneg?(s,nzv) IFF divergent?(s,nzv)

  % Time of closest approach

  tau_2D(s,nzv) : real =  -(s*nzv)/sqv(nzv)

  tau(s,v): real = IF v = zero THEN 0
                   ELSE -(s*v)/sqv(v)
                   ENDIF

  tau_is_min: LEMMA LET Tau = tau_2D(s,nzv) IN
                  is_minimum?(Tau,(LAMBDA t: sq(norm(s+t*nzv))))

  dist_tau(s,v): real = norm(s+tau(s,v)*v)

  dist_tau_min: LEMMA dist_tau(s,v) <= norm(s+t*v)

  tau_sqv_min : LEMMA sqv(s+tau(s,v)*v) <= sqv(s+t*v)

END closest_approach_relative_2D

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