SSL vectors_dot_alt.pvs
Interaktion und PortierbarkeitPVS
vectors_dot_alt[n: posnat]: THEORY %------------------------------------------------------------------------------ % The n-dimensional dot-product is defined as follows: % % Vector : TYPE = [below(n) -> real] % % *(u,v): real = sigma[below(n)](0,n-1,LAMBDA i:u(i)*v(i)) % % % For many situations this is a good definition. But, the summation % function is defined with parameter [below(n)] which can be a real nuisance when trying % to perform induction proofs (e.g. See deriv_dot_prod in the vect_analysis library). % The following alternate definition uses a sigma[nat] which eliminates this problem % though it is uglier because of the need to guard the u(j)*v(j) with an IF-THEN-ELSE %------------------------------------------------------------------------------
BEGIN
IMPORTING vectors[n], reals@sigma_nat
u,v,w : VAR Vector
i : VAR Index
dot(u,v): real = sigma[nat](0,n-1, LAMBDA (j: nat): IF j < n THEN u(j)*v(j) ELSE 0 ENDIF)
m: VAR nat
dot_rew_prep: LEMMA m < n IMPLIES
sigma[nat](0, m, LAMBDA (j: nat): IF j < n THEN u(j) * v(j) ELSE 0 ENDIF)
= sigma(0, m, LAMBDA (i: Index[n]): u(i) * v(i))
dot_rew: LEMMA dot(u,v) = u*v
END vectors_dot_alt
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
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.
