@@ -75,15 +75,15 @@ package VectorFunctions {
7575 * Scalar product of a NumericalVectorValue and a NumericalValue, which has the same value as the scalar product of the
7676 * NumericalValue and the NumericalVectorValue.
7777 */
78- abstract function vectorScalarMult specializes DataFunctions::'*' (v: NumericalVectorValue[1], x: NumericalValue[1]): NumericalVectorValue[1] {
78+ abstract function vectorScalarMult specializes DataFunctions::'*' (v: NumericalVectorValue[1], x: NumericalValue[1]) w : NumericalVectorValue[1] {
7979 scalarVectorMult(x, v)
8080 }
8181
8282 /**
8383 * Scalar quotient of a NumericalVectorValue and a NumericalValue, defined as the scalar product of the inverse of the
8484 * NumericalValue and the NumericalVectorValue.
8585 */
86- abstract function vectorScalarDiv specializes DataFunctions::'/' (v: NumericalVectorValue[1], x: NumericalValue[1]): NumericalVectorValue[1] {
86+ abstract function vectorScalarDiv specializes DataFunctions::'/' (v: NumericalVectorValue[1], x: NumericalValue[1]) w : NumericalVectorValue[1] {
8787 scalarVectorMult(1.0 / x, v)
8888 }
8989
@@ -117,13 +117,13 @@ package VectorFunctions {
117117 * Construct a CartesianVectorValue whose elements are a non-empty list of Real components.
118118 * The dimension of the NumericalVectorValue is equal to the number of components.
119119 */
120- function CartesianVectorOf(components : Real[*]) : CartesianVectorValue {
120+ function CartesianVectorOf(components: Real[*]): CartesianVectorValue {
121121 CartesianVectorValue (
122122 dimension = size(components),
123123 elements = components
124124 )
125125 }
126- function CartesianThreeVectorOf specializes CartesianVectorOf(components: Real[* ]): CartesianThreeVectorValue;
126+ function CartesianThreeVectorOf specializes CartesianVectorOf(components: Real[3 ]): CartesianThreeVectorValue;
127127
128128 /**
129129 * Cartesian zero vectors of 1, 2 and 3 dimensions.
@@ -144,15 +144,15 @@ package VectorFunctions {
144144 v.elements->forAll{in x; x == 0.0}
145145 }
146146
147- function 'cartesian+' specializes '+' (v: CartesianVectorValue[1], w: CartesianVectorValue[0..1]): CartesianVectorValue[1] {
147+ function 'cartesian+' specializes '+' (v: CartesianVectorValue[1], w: CartesianVectorValue[0..1]) u : CartesianVectorValue[1] {
148148 inv precondition { w != null implies v.dimension == w.dimension }
149149 if w == null? v
150150 else CartesianVectorOf(
151151 (1..w.dimension)->collect{in i : Positive; v[i] + w[i]}
152152 )
153153 }
154154
155- function 'cartesian-' specializes '-' (v: CartesianVectorValue[1], w: CartesianVectorValue[0..1]): CartesianVectorValue[1] {
155+ function 'cartesian-' specializes '-' (v: CartesianVectorValue[1], w: CartesianVectorValue[0..1]) u : CartesianVectorValue[1] {
156156 inv precondition { w != null implies v.dimension == w.dimension }
157157 CartesianVectorOf(
158158 if w == null? CartesianVectorOf(v.elements->collect{in x : Real; -x})
@@ -162,25 +162,25 @@ package VectorFunctions {
162162 )
163163 }
164164
165- function cartesianScalarVectorMult specializes scalarVectorMult (x: Real[1], v: CartesianVectorValue[1]): CartesianVectorValue[1] {
165+ function cartesianScalarVectorMult specializes scalarVectorMult (x: Real[1], v: CartesianVectorValue[1]) w : CartesianVectorValue[1] {
166166 CartesianVectorOf(
167167 v.elements->collect{in y : Real; x * y}
168168 )
169169 }
170- function cartesianVectorScalarMult specializes vectorScalarMult (v: CartesianVectorValue[1], x: Real[1]): CartesianVectorValue[1] {
170+ function cartesianVectorScalarMult specializes vectorScalarMult (v: CartesianVectorValue[1], x: Real[1]) w : CartesianVectorValue[1] {
171171 cartesianScalarVectorMult(x, v)
172172 }
173173
174- function cartesianInner specializes inner(v: CartesianVectorValue[1], w : CartesianVectorValue[1]): Real[1]{
174+ function cartesianInner specializes inner(v: CartesianVectorValue[1], w : CartesianVectorValue[1]) x : Real[1]{
175175 inv precondition { v.dimension == w.dimension }
176176 (1..v.dimension)->collect{in i : Positive; v[i] * w[i]}->reduce RealFunctions::'+'
177177 }
178178
179- function cartesianNorm specializes norm(v: CartesianVectorValue[1]) : NumericalValue[1] {
179+ function cartesianNorm specializes norm(v: CartesianVectorValue[1]) l : NumericalValue[1] {
180180 sqrt(cartesianInner(v, v))
181181 }
182182
183- function cartesianAngle specializes angle(v: CartesianVectorValue[1], w: CartesianVectorValue[1]): Real[1] {
183+ function cartesianAngle specializes angle(v: CartesianVectorValue[1], w: CartesianVectorValue[1]) theta : Real[1] {
184184 inv precondition { v.dimension == w.dimension }
185185 arccos(cartesianInner(v, w) / (norm(v) * norm(w)))
186186 }
0 commit comments