Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: topology_prelim.prf   Sprache: PVS

Untersuchung PVS©

intersections_2D: THEORY
%--------------------------------------------------------------------------
%
%  Derived from paper "Intersection of Linear and Circular Components in 2D"
%  by David Eberly. Available at:
%
%    www.magic-software.com
%
%  Author: Ricky Butler              NASA Langley Research Center
%
%--------------------------------------------------------------------------
BEGIN

   IMPORTING distance_2D,
             det_2D,
             lines_2D, parallel_2D

   p,p0,p1,p2,pnot,u,v,v0,v1,v2: VAR Vect2

   s,t,t1,t2: VAR real

   nza: VAR nzreal

   cross(p0,p1): MACRO real = det(p0,p1)
 
%                                     |     Basic        |   Parametric
%                                     |------------------|-----------------
%   Line : TYPE = [# p: Vect2,        | point on the line| position at time 0
%                    v: Nz_vect2 #]   | direction vector | velocity vector


%  Let L0 = p0 + s*v  == L0`p + s*L0`v
%  Let L1 = p0 + s*v1 == L1`p + s*L1`v


   L0,L1: VAR Line2D

   det_line: LEMMA LET DELTA = L1`p - L0`p IN
                     L0`p + s*L0`v =  L1`p + t*L1`v IMPLIES
                        det(L0`v,L1`v)*s = det(DELTA,L1`v) AND
                        det(L0`v,L1`v)*t = det(DELTA,L0`v)

%  Three cases
%      intersecting :   det(L0`v,L1`v) /= 0 
%      parallel     :   det(L0`v,L1`v) =  0 AND det(DELTA,L0`v) /= 0
%      same_line    :   det(L0`v,L1`v) =  0 AND det(DELTA,L0`v) = 0


   intersect?(L0,L1): bool = det(L0`v,L1`v) /= 0 

   same_line?(L0,L1): bool = LET DELTA = L1`p - L0`p IN  
                               det(L0`v,L1`v) = 0 AND det(DELTA,L0`v) = 0
%  ----------- function to return intersection point --------------

    intersect_pt(L0:Line2D,L1: Line2D | det(L0`v,L1`v) /= 0): Vect2 =
                               LET DELTA = L1`p - L0`p,
                                   ss = det(DELTA,L1`v)/det(L0`v,L1`v) IN 
                                   L0`p + ss*L0`v

%  ----------- basic properties ---------------

   IMPORTING parallel_2D

   same_line_sym: LEMMA same_line?(L0,L1) IMPLIES same_line?(L1,L0)  

   intersect_not_parallel: LEMMA intersect?(L0,L1) IMPLIES
                                   NOT parallel?(L0`v,L1`v)

   intersection_lem      : LEMMA det(L0`v,L1`v) /= 0 IMPLIES
                                    LET DELTA = L1`p - L0`p,
                                       ss = det(DELTA,L1`v)/det(L0`v,L1`v),
                                       tt = det(DELTA,L0`v)/det(L0`v,L1`v)
                                    IN
                              L0`p + ss*L0`v =  L1`p + tt*L1`v

   lines_intersection(so:Vect2,vo:Nz_vect2,si:Vect2,vi:Nz_vect2|det(vo,vi) /= 0) : [real,real] =
     LET ns = si-so,
         d = det(vo,vi) IN
     (det(ns,vi)/d, det(ns,vo)/d)

   lines_intersection_sound : LEMMA
     FORALL(so:Vect2,vo:Nz_vect2,si:Vect2,vi:Nz_vect2|det(vo,vi) /= 0):
       LET (ko,ki) = lines_intersection(so,vo,si,vi) IN
       so+ko*vo = si+ki*vi

    pt_intersect          : LEMMA on_line?(p,L0) AND on_line?(p,L1) AND
                                 NOT same_line?(L0,L1) IMPLIES
                                     intersect?(L0,L1) 


   intersect_pt_unique   : LEMMA intersect?(L0,L1) IMPLIES
                                 pnot /= intersect_pt(L0,L1) AND
                                 on_line?(pnot,L0)  
                              IMPLIES
                                 NOT on_line?(pnot,L1)

   same_line_lem         : LEMMA p0 /= p1 AND
                                ( on_line?(p0,L0) AND on_line?(p0,L1) AND
                                  on_line?(p1,L0) AND on_line?(p1,L1) )
                                     IMPLIES same_line?(L0,L1)
        
   not_same_line         : LEMMA on_line?(p,L0) AND NOT on_line?(p,L1) IMPLIES
                                 NOT same_line?(L0,L1)
                         
 
   intersect_pt_lem      : LEMMA NOT same_line?(L0,L1) AND
                                 on_line?(pnot,L0)  AND
                                 on_line?(pnot,L1)  
                              IMPLIES
                                  intersect_pt(L0,L1) = pnot 
                       
END intersections_2D



¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.29Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik