| 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 vect2D.pvs Sprache: PVS |
|||||||||
|
vect2D : THEORY
%------------------------------------------------------------------------------ % % This theory creates a special 2D version of vectors from the generic vectors % library by importing vectors[2]. Note that this is nearly equivalent % to the vectors_2D 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(2) % Vector : TYPE = [Index -> real] % % and the record structure of vectors_2D: % % Vect2: TYPE = [# x, y: real #] % %------------------------------------------------------------------------------ BEGIN IMPORTING vectors[2] Vect2 : TYPE = Vector x,y : VAR real u,v : VAR Vect2 vect2(x,y): Vect2 = LAMBDA(i:Index): IF i=0 THEN x ELSE y ENDIF put_x(v,x): Vect2 = v WITH [`0 := x] put_y(v,y): Vect2 = v WITH [`1 := y] x(v) : MACRO real = v(0) y(v) : MACRO real = v(1) iv : Vect2 = vect2(1,0) jv : Vect2 = vect2(0,1) vect2D_0 : LEMMA vect2(x,y)(0) = x vect2D_1 : LEMMA vect2(x,y)(1) = y eq2D?(u,v): bool = x(u)=x(v) AND y(u) = y(v) Eq2D : LEMMA eq2D?(u,v) IFF u = v pp2D(v) :[real,real] = (x(v),y(v)) END vect2D ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28