products/sources/formale Sprachen/Coq/tools/coqdoc/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: gs_line.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% 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

[ Dauer der Verarbeitung: 0.2 Sekunden  (vorverarbeitet)  ]