|
%------------------------------------------------------------------------------
% gs_line.pvs
% ACCoRD v.1.0
%
% Ground speed line solutions are ground speed only solutions that are tangent
% to the protected zone.
%------------------------------------------------------------------------------
gs_line[D: posreal] : THEORY
BEGIN
IMPORTING gs_only[D],
tangent_line[D]
sp : VAR Sp_vect2
eps : VAR Sign
vo,vi,
nvo : VAR Vect2
%------------%
% ALGORITHMS %
%------------%
% zero indicates no ground speed solution
gs_line_eps(sp,vo,vi,eps): {nvo | nz_vect2?(nvo) =>
gs_only?(vo)(nvo)} =
LET (k,nvo) = gs_only_line(tangent_line(sp,eps),vo,vi) IN
IF k >= 0 THEN
nvo
ELSE
zero
ENDIF
gs_line_eps?(sp,vo,vi,eps)(nvo) : bool =
nz_vect2?(nvo) AND
nvo = gs_line_eps(sp,vo,vi,eps)
gs_line?(sp,vo,vi)(nvo):bool =
nz_vect2?(nvo) AND
EXISTS (eps): nvo = gs_line_eps(sp,vo,vi,eps)
%----------%
% LEMMAS %
%----------%
gs_line_eps_tangent_line: LEMMA
gs_line_eps?(sp,vo,vi,eps)(nvo)
IMPLIES
tangent_line?(sp,nvo-vi,eps)
gs_line_is_line_solution: LEMMA
gs_line_eps?(sp,vo,vi,eps)(nvo)
IMPLIES
line_solution?(sp,nvo-vi,eps)
two_parallel?(sp,vo,vi) : bool =
det(vi,vo) = 0 AND
EXISTS (eps:Sign): det(vo,tangent_line(sp,eps)) = 0
gs_line_complete : LEMMA
gs_only?(vo)(nvo) AND
NOT two_parallel?(sp,vo,vi) AND
line_solution?(sp,nvo-vi) IMPLIES
gs_line?(sp,vo,vi)(nvo)
END gs_line
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
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
|
