| products/sources/formale sprachen/Isabelle/Doc/Corec/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: BExp.pvs Sprache: PVSOriginal von: 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 ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
