23 #ifndef SHEAF_DLL_SPEC_H 24 #include "SheafSystem/sheaf_dll_spec.h" 27 #ifndef ASSERT_CONTRACT_H 28 #include "SheafSystem/assert_contract.h" 32 #include "SheafSystem/sec_ed.h" 143 template <
typename S,
typename SR>
144 void dot(
const S& x0,
const S& x1, SR& xresult,
bool xauto_access)
148 require(x0.state_is_auto_read_accessible(xauto_access));
149 require(x1.state_is_auto_read_accessible(xauto_access));
150 require(x0.is_same_type(&x1));
151 require(x0.is_p_form(xauto_access) == x1.is_p_form(xauto_access));
157 x0.get_read_access();
158 x1.get_read_access();
161 typedef typename S::fiber_type::volatile_type V;
162 typedef typename SR::fiber_type::volatile_type VR;
163 dot_functor<V, VR> f;
164 binary_op(x0, x1, xresult, f, xauto_access);
180 template <
typename S,
typename SR>
181 void length(
const S& x0, SR& xresult,
bool xauto_access)
185 require(x0.state_is_auto_read_accessible(xauto_access));
191 x0.get_read_access();
194 typedef typename S::fiber_type::volatile_type V;
195 typedef typename SR::fiber_type::volatile_type VR;
196 length_functor<V, VR> f;
197 unary_op(x0, xresult, f, xauto_access);
212 template <
typename S>
217 require(x0.state_is_auto_read_write_accessible(xauto_access));
218 ensure(xlength >= 0.0);
224 x0.get_read_write_access(
true);
227 put_length_functor<typename S::fiber_type::volatile_type> f;
228 unary_op(x0, xlength, f, xauto_access);
237 ensure(unexecutable(
"length(x0, xauto_access) == xlength"));
245 template <
typename S,
typename SR>
246 void normalize(
const S& x0, SR& xresult,
bool xauto_access)
250 require(x0.state_is_auto_read_accessible(xauto_access));
251 require(xresult.state_is_auto_read_write_accessible(xauto_access));
252 require(x0.is_same_type(&xresult));
253 require(x0.is_p_form(xauto_access) == xresult.is_p_form(xauto_access));
259 x0.get_read_access();
260 xresult.get_read_write_access(
true);
263 normalize_functor<typename S::fiber_type::volatile_type> f;
264 unary_op(x0, xresult, f, xauto_access);
269 xresult.release_access();
274 ensure(xresult.is_p_form(xauto_access) == x0.is_p_form(xauto_access));
275 ensure(unexecutable(
"length(xresult, xauto_access) == 1.0"));
283 template <
typename T>
288 require(precondition_of(
normalize(x0, x0, xauto_access)));
296 ensure(postcondition_of(
normalize(x0, x0, xauto_access)));
303 #endif // ifndef SEC_ED_IMPL_H void length(const S &x0, SR &xresult, bool xauto_access)
void unary_op(const S0 &x0, SR &xresult, F xfunctor, bool xauto_access)
Unary operator.
void normalize(const S &x0, SR &xresult, bool xauto_access)
void binary_op(const S0 &x0, const S1 &x1, SR &xresult, F xfunctor, bool xauto_access)
Binary operator.
void dot(const S &x0, const S &x1, SR &xresult, bool xauto_access)
void put_length(S &x0, const vd_value_type &xlength, bool xauto_access)
Namespace for the fiber_bundles component of the sheaf system.
double vd_value_type
The type of component in the fiber; the scalar type in the fiber vector space.