| 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 fseqs_ops_vect3.pvs Sprache: PVS |
|||||||||
|
fseqs_ops_vect3: THEORY
%------------------------------------------------------------------------ % % Defines some convenient operations over finite sequences of Vect3 % % EXPERIMENTAL % %------------------------------------------------------------------------ BEGIN IMPORTING vectors_3D, structures@fseqs_ops[Vect3] fs,gs: VAR fseq[Vect3] nefs: VAR ne_fseq[Vect3] i,n: VAR nat x: VAR real % ------------ pointwise addition, subtraction of a sequence of vectors mmin(m,n:nat): MACRO nat = IF m > n THEN n ELSE m ENDIF ; +(fs,gs): fseq[Vect3] = LET len = mmin(l(fs),l(gs)) IN (# length := len, seq := (LAMBDA n: IF n < len THEN fs(n) + gs(n) ELSE default ENDIF) #) ; -(fs,gs): fseq[Vect3] = LET len = mmin(l(fs),l(gs)) IN (# length := len, seq := (LAMBDA n: IF n < len THEN fs(n) + gs(n) ELSE default ENDIF) #) ; % ---------- scalar product of a sequence of reals with a sequence of vectors IMPORTING structures@fseqs_ops_real c: VAR fseq[real] *(c,gs): fseq[Vect3] = (# length := l(gs), seq := (LAMBDA n: IF n < l(gs) THEN c(n) * gs(n) ELSE default ENDIF) #) ; END fseqs_ops_vect3 ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28