20 #ifndef SEC_ST2_IMPL_H 21 #define SEC_ST2_IMPL_H 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_st2.h" 44 template <
typename V0,
typename VR>
46 trace_functor<V0, VR>::
47 operator()(
const V0& x0, VR& xresult)
51 require(precondition_of(xresult =
trace(x0)));
60 ensure(postcondition_of(xresult =
trace(x0)));
68 template <
typename V0,
typename VR>
70 determinant_functor<V0, VR>::
71 operator()(
const V0& x0, VR& xresult)
75 require(precondition_of(xresult =
determinant(x0)));
81 xresult.put_component(0, lcomp);
87 ensure(postcondition_of(xresult =
determinant(x0)));
98 template <
typename S0,
typename SR>
99 void trace(
const S0& x0, SR& xresult,
bool xauto_access)
103 require(x0.state_is_auto_read_accessible(xauto_access));
109 x0.get_read_access();
112 typedef typename S0::fiber_type::volatile_type V0;
113 typedef typename SR::fiber_type::volatile_type VR;
114 trace_functor<V0, VR> f;
115 unary_op(x0, xresult, f, xauto_access);
130 template <
typename S0,
typename SR>
135 require(x0.state_is_auto_read_accessible(xauto_access));
141 x0.get_read_access();
144 typedef typename S0::fiber_type::volatile_type V0;
145 typedef typename SR::fiber_type::volatile_type VR;
146 determinant_functor<V0, VR> f;
147 unary_op(x0, xresult, f, xauto_access);
163 #endif // ifndef SEC_ST2_IMPL_H void unary_op(const S0 &x0, SR &xresult, F xfunctor, bool xauto_access)
Unary operator.
void trace(const S0 &x0, SR &xresult, bool xauto_access)
void determinant(const S0 &x0, SR &xresult, 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.