products/sources/formale Sprachen/PVS/ACCoRD/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: circle_solutions.pvs   Sprache: PVS

Original von: PVS©
%------------------------------------------------------------------------------
% line_solutions.pvs
% ACCoRD v1.0
%
% Circle solutions are vectors v such that at time t the ownship is on the 
% circle of radius D and altitude H. If dir=-1, v points into the circle and 
% outside the rectangle; if dir=1, v points outside the circle and inside the
% rectangle.
%------------------------------------------------------------------------------

circle_solutions[D,H:posreal] : THEORY
BEGIN

  IMPORTING circle_criterion[D,H]

  s,v     : VAR Vect3
  t       : VAR real
  dir,eps : VAR Sign
  pt      : VAR posreal

  circle_solution?(s,v,t,dir): bool =
    t > 0 AND
    circle_solution_2D?(s,v,t,dir) AND
    vertical_solution?(s`z,v`z,t,-dir)

  circle_solution_horizontal: LEMMA
    vertical_conflict?(s`z,v`z) AND
    circle_solution?(s,v,t,dir) 
    IMPLIES
      v`z /= 0 AND circle_solution?(s,v,Theta_H(s`z,v`z,-dir),dir)

  circle_solution_vertical: LEMMA
    horizontal_conflict?(s,v) AND
    circle_solution?(s,v,t,dir) 
    IMPLIES
      NOT zero_vect2?(v) AND circle_solution?(s,v,Theta_D(s,v,dir),dir)

  circle_solution_meets_criterion : LEMMA
    circle_solution?(s,v,t,dir) IMPLIES
    circle_criterion_at?(s,v,t,dir)

  circle_solution_independence : THEOREM
    circle_solution?(s,v,t,dir) IMPLIES
    NOT conflict_ever?(s,v)

  circle_solution?(s,v): MACRO bool =
    EXISTS (dir,t): circle_solution?(s,v,t,dir)


END circle_solutions

¤ Dauer der Verarbeitung: 0.15 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff