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


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Fortran/f90gl-1.2.15/examples/ (NIST Fortran ^©) Datei vom 8.0.2004 mit Größe 3 kB

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.