Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: make-one-time-file.py Sprache: PVS

Original von: PVS^©

circles_and_lines: THEORY
%------------------------------------------------------------------------
%
%  ------ Intersection of parametric line and a circle -----
%
%  See related theorems in vectors@closest_approach_2D
%
%  Author: Cesar Munoz           National Institute for Aerospace
%
%------------------------------------------------------------------------
BEGIN

  IMPORTING quad_minmax

  sx,sy,vx,vy   : VAR real

  % The first lemma states that if t1 and t2 are the intersection
  % points with a circle of radius D, then the distance for all times
  % between t1 and t2 is less than D

  t1_lt_t2_lt_D : LEMMA FORALL (t,t1,t2,D:real):
                  vx*vx + vy*vy /= 0 AND
                  t1 < t2 AND
                  (sx+vx*t1)*(sx+vx*t1) + (sy+vy*t1)*(sy+vy*t1) = D AND
                  (sx+vx*t2)*(sx+vx*t2) + (sy+vy*t2)*(sy+vy*t2) = D AND
                  t1 < t AND t < t2 IMPLIES
                  (sx+vx*t)*(sx+vx*t) + (sy+vy*t)*(sy+vy*t) < D

  % The second lemma is the reciprocal of the previous lemma. It states that
  % if the distance at time t is less than D, then t is between t1 and
  % t2.

  lt_D_t1_lt_t2 : LEMMA FORALL (t,t1,t2,D:real):
                  vx*vx + vy*vy /= 0 AND
                  t1 < t2 AND
                  (sx+vx*t1)*(sx+vx*t1) + (sy+vy*t1)*(sy+vy*t1) = D
                  AND
                  (sx+vx*t2)*(sx+vx*t2) + (sy+vy*t2)*(sy+vy*t2) = D
                  AND
                  (sx+vx*t)*(sx+vx*t) + (sy+vy*t)*(sy+vy*t) < D IMPLIES
                  t1 < t AND t < t2

  % The third lemma states that if there are no intersection points with
  % a circle of radius D then the distance at any time is greater than D.

  discr_le_0 : LEMMA FORALL (t,discrm,D:real):
           discrm = 2*sx*vx*sy*vy + D*(vx*vx+vy*vy) -
                    (sx*sx*vy*vy + sy*sy*vx*vx) AND
           discrm <= 0 AND vx*vx + vy*vy /= 0
           IMPLIES
           (sx+vx*t)*(sx+vx*t) + (sy+vy*t)*(sy+vy*t) >= D

END circles_and_lines

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.