Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vect3D.pvs Sprache: PVS

Original von: 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.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.