products/sources/formale sprachen/Cobol/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: between_2D.pvs   Sprache: Unknown

between_2D: THEORY
%------------------------------------------------------------------------------
%
%    Provides:
%       between?(v1,v2)(xx)  -- true iff xx is between? v1 and v2 (within 180 of each other)
%       betw?(v1,v2)(xx)     -- true iff xx is between? v1 and v2
%
%    Author:
%        Rick Butler            NASA Langley Research Center
%
%    VERY EXPERIMENTAL !!!!
%
%------------------------------------------------------------------------------
BEGIN

   %% --------- between? assuming v1 and v2 are within 180 of each other ----------

   IMPORTING vectors_2D, trig@trig_basic, trig@trig_ineq, angles_2D

   between?(v1,v2: Vect2)(xx: Vect2): bool =
       LET k1 = norm(v1),
           k2 = norm(v2),
           kx = norm(xx) IN
          v1*(kx*v2-k2*xx) <= 0 AND
          v2*(kx*v1-k1*xx) <= 0 

   a1,a2,a3: VAR real
   v,v1,v2,v3: VAR Vect2
   k: VAR posreal
   k1,k2,k3: VAR posreal

   between_sym: LEMMA between?(v1,v3)(v2) IFF between?(v3,v1)(v2) 


   between_cos: LEMMA LET v1 = v_from(a1,k1),
                          v2 = v_from(a2,k2),
                          v3 = v_from(a3,k3) IN
                      between?(v1,v3)(v2) IFF
                          ( cos(a3 - a1) <= cos(a3 - a2) AND
                            cos(a3 - a1) <= cos(a2 - a1) )

   is_between: LEMMA  a1 <= a2 AND a2 <= a3 AND
                      a3 - a1 <= pi AND a2 - a1 <= pi
                   IMPLIES
                      LET v1 = v_from(a1,k1),
                          v2 = v_from(a2,k2),
                          v3 = v_from(a3,k3) IN
                        between?(v1,v3)(v2)


   is_between2: COROLLARY 0 <= a1 AND a1 <= a2 AND a2 <= a3 AND a3 <= pi IMPLIES
                    LET v1 = v_from(a1,k1),
                        v2 = v_from(a2,k2),
                        v3 = v_from(a3,k3) IN
                    between?(v1,v3)(v2)


   between_lem: LEMMA LET v1 = v_from(a1,k1),
                       v2 = v_from(a2,k2),
                       v3 = v_from(a3,k3) IN
                    0 <= a1 AND a1 <= pi AND
                    0 <= a2 AND a2 <= pi AND
                    0 <= a3 AND a3 <= pi AND
                    a1 <= a3 AND
                    between?(v1,v3)(v2)
                        IMPLIES (a1 <= a2 AND a2 <= a3) 


   between_thm: THEOREM LET v1 = v_from(a1,k1),
                       v2 = v_from(a2,k2),
                       v3 = v_from(a3,k3) IN
                    0 <= a1 AND a1 <= pi AND
                    0 <= a2 AND a2 <= pi AND
                    0 <= a3 AND a3 <= pi AND
                    between?(v1,v3)(v2)
                        IMPLIES (a1 <= a2 AND a2 <= a3) OR
                                (a3 <= a2 AND a2 <= a1)


%% ------------ betw ----------------

   betw?(v1,v2: Nz_vect2)(xx: Nz_vect2): bool =
           angle(v1) <= angle(xx) AND angle(xx) <= angle(v2)


   betw_between: LEMMA FORALL (v1,v2,xx: Nz_vect2):
                          angle(v2) - angle(v1) <= pi AND 
                          angle(xx) - angle(v1) <= pi AND
                          betw?(v1,v2)(xx) IMPLIES between?(v1,v2)(xx)

   between_betw: LEMMA FORALL (v1,v2,xx: Nz_vect2):
                       angle(v1) <= pi AND angle(xx) <= pi AND angle(v2) <= pi AND
                       angle(v1) <= angle(v2) AND
                       between?(v1,v2)(xx) IMPLIES betw?(v1,v2)(xx) 

END between_2D

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]