Quelle trk_bands_2D.pvs Sprache: PVS

%-----------------------------------------------------------------------------
% trk_bands_2D.pvs
% ACCoRD v.1.0
%-----------------------------------------------------------------------------

trk_bands_2D[D:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY
BEGIN

  IMPORTING analysis@interm_value_thm,
       vect_analysis@vect2_cont_dot[real],
            trig_fnd@sincos,
            omega_v2[D,B,T],
            trk_line[D],
     line_solutions[D],
            bands_util

  nvo,
  vo,vi : VAR Nz_vect2
  sp    : VAR Sp_vect2
  ss    : VAR Ss_vect2
  t     : VAR posreal
  band  : VAR ConnectedGeLt(0,2*pi)
  trk   : VAR real % Track with respect to true north.
  k     : VAR real

  pm,eps,
  irt,
  irt1,
  irt2   : VAR Sign
  s,
  nvo1,
  nvo2   : VAR Vect2

  trk_band : LEMMA
     nvo = trk_line_eps_irt(ss, vo, vi, eps, irt) IMPLIES
     eps*det(nvo,ss) >= eps*det(vi,ss)

  trk2v2_continuous : JUDGEMENT
    trk2v2(vo) HAS_TYPE continuous_rv_fun

  Vtrk_continuous : JUDGEMENT
    Vtrk(vo,vi) HAS_TYPE continuous_rv_fun

  %-----------------------------------------------%
  % 2-D Track Critical Points                     %
  %-----------------------------------------------%

  trk_critical?(s,vo,vi)(trk) : bool =
    LET trko = trk2v2(vo)(trk) IN
    (sqv(s)>=sq(D) AND trk_line?(s,vo,vi)(trko)) OR
    trk_only_circle?(s,vo,vi,T,Entry)(trko) OR
    (B>0 AND trk_only_circle?(s,vo,vi,B,Exit)(trko))

  Omega_trk_spc(vo,vi,t)(trk) : real =
    vi * trk2v2(vo)(trk) - sq(D/t)

  Omega_trk_spc : JUDGEMENT
    Omega_trk_spc(vo,vi,t) HAS_TYPE (continuous_rr?)

  trk_special_case_invariant: LEMMA
    trk_special_case?(s,vo,vi,t) IFF
    trk_special_case?(s,trk2v2(vo)(trk),vi,t)

  Omega_trk_spc_separated : LEMMA
    Omega_trk_spc(vo,vi,t)(trk) = 0 AND
    trk_special_case?(s,vo,vi,t) IMPLIES
    sqv(s)>=sq(D)

  Omega_trk_spc_critical : LEMMA
    Omega_trk_spc(vo,vi,t)(trk) = 0 AND
    trk_special_case?(s,vo,vi,t) IMPLIES
    line_solution?(s,Vtrk(vo,vi)(trk))

  trk_special_case_conflict_T : LEMMA
    trk_special_case?(s,vo,vi,T) IMPLIES
    (horizontal_entry_at?(s,Vtrk(vo,vi)(trk),T)
     IFF NOT conflict_2D?(s,Vtrk(vo,vi)(trk)))

  trk_special_case_conflict_B : LEMMA
    B>0 AND trk_special_case?(s,vo,vi,B) IMPLIES
    (horizontal_exit_at?(s,Vtrk(vo,vi)(trk),B)
     IFF NOT conflict_2D?(s,Vtrk(vo,vi)(trk)))

  Omega_trk_spc_conflict_T: LEMMA
    trk_special_case?(s,vo,vi,T) IMPLIES
    (Omega_trk_spc(vo,vi,T)(trk) < 0 IFF
    conflict_2D?(s,Vtrk(vo,vi)(trk)))

  Omega_trk_spc_conflict_B: LEMMA
    B>0 AND trk_special_case?(s,vo,vi,B) IMPLIES
    (-Omega_trk_spc(vo,vi,B)(trk) < 0 IFF
    conflict_2D?(s,Vtrk(vo,vi)(trk)))

  Omega_trk(s,vo,vi) : (continuous_rr?) =
    omega_v2(s) o Vtrk(vo,vi)

  Omega_trk_critical : LEMMA
    Omega_trk(s,vo,vi)(trk) = 0 AND
    NOT trk_special_case?(s,vo,vi,T) AND
    NOT (B>0 AND trk_special_case?(s,vo,vi,B)) IMPLIES
      trk_critical?(s,vo,vi)(trk)

  % Bands do not contain critical points
  trk_band?(s,vo,vi)(band) : bool =
    FORALL (trko:(band)) :
      NOT trk_critical?(s,vo,vi)(trko)

  trk_green?(s,vo,vi)(band) : bool =
    FORALL (trko:(band)) :
      NOT conflict_2D?(s,Vtrk(vo,vi)(trko))

  trk_red?(s,vo,vi)(band) : bool =
    FORALL (trko:(band)) :
      conflict_2D?(s,Vtrk(vo,vi)(trko))

  trk_line_sort_eps : LEMMA
    nvo /= vi AND
    trk_line_eps_irt?(ss,vo,vi,eps,irt)(nvo) IMPLIES
    eps*det(nvo,ss) > eps*det(vi,ss)

  trk_line_sort_eps_angle : LEMMA
    abs(det(vi,ss)/(norm(vo)*norm(ss))) <= 1 IMPLIES
    LET phi   = track(ss),
        psi   = asin(det(vi,ss)/(norm(vo)*norm(ss))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    nvo1 /= vi AND
    nvo2 /= vi AND
    trk_line_eps_irt?(ss,vo,vi,1,irt1)(nvo1) AND
    trk_line_eps_irt?(ss,vo,vi,-1,irt2)(nvo2)
    IMPLIES
      to2pi(track(nvo1)-alpha) < to2pi(track(nvo2)-alpha)

  trk_line_sort_eps_1_angle_case1 : LEMMA
    abs(det(vi,ss)/(norm(vo)*norm(ss))) <= 1 IMPLIES
    LET phi   = track(ss),
        psi   = asin(det(vi,ss)/(norm(vo)*norm(ss))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (nvo1*ss) * (nvo2*ss) < 0 AND
    nvo1 /= vi AND
    nvo2 /= vi AND
    trk_line_eps_irt?(ss,vo,vi,1,-1)(nvo1) AND
    trk_line_eps_irt?(ss,vo,vi,1,1)(nvo2)
    IMPLIES
      to2pi(track(nvo1)-alpha) < to2pi(track(nvo2)-alpha)

  trk_line_sort_eps_1_angle_case2 : LEMMA
    abs(det(vi,ss)/(norm(vo)*norm(ss))) <= 1 IMPLIES
    LET phi   = track(ss),
        psi   = asin(det(vi,ss)/(norm(vo)*norm(ss))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (nvo1*ss) * (nvo2*ss) >= 0 AND
    nvo1 /= vi AND
    nvo2 /= vi AND
    trk_line_eps_irt?(ss,vo,vi,1,-1)(nvo1) AND
    trk_line_eps_irt?(ss,vo,vi,1,1)(nvo2)
    IMPLIES
      (det(nvo1,nvo2) < 0 IFF to2pi(track(nvo1)-alpha) < to2pi(track(nvo2)-alpha))

  trk_line_color : LEMMA
    trk_line_eps_irt?(ss,vo,vi,eps,irt)(nvo) AND
    sq(Qs(ss,eps)*vi) > (sqv(ss)-sq(D))*(sqv(vi)-sqv(vo))
    IMPLIES
    (pm*(Q(ss,eps) * perpR(nvo)) > 0 IFF pm*(eps*irt) < 0)

  %-------------------------------------------%
  % THEOREM: Track Green Bands Correctness    %
  %-------------------------------------------%

  trk_green_band : THEOREM
    FORALL (trko:(band)) :
       trk_band?(s,vo,vi)(band) IMPLIES
        (NOT cd2d?(s,Vtrk(vo,vi)(trko)) IFF
         trk_green?(s,vo,vi)(band))

  %-------------------------------------------%
  % THEOREM: Track Red Bands Correctness      %
  %-------------------------------------------%

  trk_red_band : THEOREM
    FORALL (trko:(band)) :
      trk_band?(s,vo,vi)(band) IMPLIES
      (cd2d?(s,Vtrk(vo,vi)(trko)) IFF
        trk_red?(s,vo,vi)(band))

END trk_bands_2D

quality91%

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

Die farbliche Syntaxdarstellung ist noch experimentell.