|
%------------------------------------------------------------------------------
% vertical_cr.pvs
% ACCoRD v.1.0
% Vertical resolution algorithm
%------------------------------------------------------------------------------
vertical_cr[D,H: posreal] : THEORY
BEGIN
IMPORTING vs_circle[D,H],
gs_circle[D,H],
trk_circle[D,H],
opt_vertical[D,H]
sp : VAR Sp_vect3 % 3-D separation
nvo : VAR Vect3
vo,vi : VAR Nzv2_vect3
epsh,epsv : VAR Sign
%------------%
% ALGORITHMS %
%------------%
hor_circle?(sp,vo,vi,epsh,epsv)(nvo) : bool =
gs_vertical?(sp,vo,vi,epsh,epsv)(nvo) OR
trk_vertical?(sp,vo,vi,epsh,epsv)(nvo) OR
opt_vertical?(sp,vo,vi,epsh,epsv)(nvo)
hor_circle_horizontal_only : LEMMA
hor_circle?(sp,vo,vi,epsh,epsv)(nvo) IMPLIES
horizontal_only?(vo)(nvo)
vertical_cr?(sp,vo,vi,epsh,epsv)(nvo) : bool =
vs_circle?(sp,vo,vi,epsv)(nvo) OR
hor_circle?(sp,vo,vi,epsh,epsv)(nvo)
vertical_cr_meets_vertical_criterion: THEOREM
horizontal_conflict?(sp,vo-vi) AND
vertical_cr?(sp,vo,vi,epsh,epsv)(nvo)
IMPLIES
vertical_criterion?(epsv)(sp,vo-vi)(nvo-vi)
hor_circle_meets_horizontal_criterion: THEOREM
horizontal_sep?(sp) AND
hor_circle?(sp,vo,vi,epsh,epsv)(nvo)
IMPLIES
horizontal_criterion?(sp,epsh)(nvo-vo)
END vertical_cr
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
