Quelle circle_criterion.pvs Sprache: PVS

%------------------------------------------------------------------------------
% circle_criterion.pvs
% ACCoRD v1.0
%
%------------------------------------------------------------------------------

circle_criterion[D,H: posreal]: THEORY
BEGIN

  IMPORTING space_3D[D,H],
            horizontal_criteria[D],
            vz_criteria[H]

  spz     : VAR Spz_vect3   % Vertically separated
  vzgs    : VAR Zv2_vect3   % Ground speed is zero
  s,v     : VAR Vect3
  eps,dir : VAR Sign
  t       : VAR real

  %% Vertical separation
  vertical_sep_independence : THEOREM
    vertical_exit?(spz`z,v`z)
    IMPLIES
      NOT conflict?(spz,v)

  %% Ground speed is 0

  nogs_criterion?(s,vzgs): bool =
    vertical_sep?(s`z) AND vertical_exit?(s`z,vzgs`z) OR
    horizontal_sep?(s)

  nogs_criterion_independence : THEOREM
    nogs_criterion?(s,vzgs) IFF NOT conflict?(s,vzgs)

  %% Aircarft are separated
  circle_criterion?(s,v,dir): bool =
    horizontal_sep?(s) AND
    vertical_sep?(s`z) AND
    horizontal_dir?(s,v,dir) AND
    vertical_dir?(s`z,v`z,-dir)

  circle_criterion_at?(s,v,t,dir): MACRO bool =
    circle_criterion?(s+t*v,v,dir)

  circle_criterion_independence : THEOREM
    circle_criterion?(s,v,dir) IMPLIES
      NOT conflict_ever?(s,v)

  circle_criterion_at_independence: THEOREM
    circle_criterion_at?(s,v,t,dir)
    IMPLIES
      NOT conflict_ever?(s,v)

END circle_criterion

quality97%

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