Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vect2D.pvs Sprache: PVS

Original von: 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.1 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.