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

quality85%

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

sprechenden Kalenders