|
%------------------------------------------------------------------------------
% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
