| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle vect3D.pvs Sprache: PVS |
|||||||||
|
vect3D : THEORY
%------------------------------------------------------------------------------ % % This theory creates a special 3D version of vectors from the generic vectors % library by importing vectors[3]. Note that this is nearly equivalent % to the vectors_3D library. Since lemma names are the same this theory % it is hoped that switching between them will be seemless. This theory % seeks to bridge the gap between the generic vectors type: % % Index : TYPE = below(3) % Vector : TYPE = [Index -> real] % % and the record structure of vectors_3D: % % Vect3: TYPE = [# x, y, z: real #] % %------------------------------------------------------------------------------ BEGIN IMPORTING vectors[3] Vect3 : TYPE = Vector x,y,z : VAR real u,v : VAR Vect3 vect3(x,y,z) : Vect3 = LAMBDA(i:Index): IF i=0 THEN x ELSIF i=1 THEN y ELSE z ENDIF put_x(v,x) : Vect3 = v WITH [`0 := x] put_y(v,y) : Vect3 = v WITH [`1 := y] put_z(v,z) : Vect3 = v WITH [`2 := z] x(v) : MACRO real = v(0) y(v) : MACRO real = v(1) z(v) : MACRO real = v(2) % --------- Basis vectors iv : Vect3 = vect3(1,0,0) jv : Vect3 = vect3(0,1,0) kv : Vect3 = vect3(0,0,1) % ----------- Equality eq3D?(u,v): bool= x(u)=x(v) AND y(u) = y(v) AND z(u)=z(v) Eq3D : LEMMA eq3D?(u,v) IFF u = v vect3D_0 : LEMMA vect3(x,y,z)(0) = x vect3D_1 : LEMMA vect3(x,y,z)(1) = y vect3D_2 : LEMMA vect3(x,y,z)(2) = z pp3D(v) :[real,real,real] = (x(v),y(v),z(v)) END vect3D ¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28