Model methods with bodies and specifications do not have
any runtime-assertion checking code created for them,
and hence there is no check that the specs are correcct
or honored.
There are some legitimate alternatives to the "no check"
option, all of which are more useful than nothing in my
opinion. The two that I like are:
1. Check to an arbitrary, user-defined (with a default) but
finite recursion depth. Some Eiffel systems support this
option.
2. A language I helped develop called JJ had two aspects
that supported this feature:
a. visibility of methods in dependent checks impacted
assertion checking --- if a method with wider visibility
called a method (normal or model) with narrower visibility
(e.g., public to private), then then assertion was not
checked. In all other cases (narrow to wide or equal) it was.
b. call trace analysis (track all call traces through the
infrastructure and do cycle detection)
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Logged In: YES
user_id=42011
There are some legitimate alternatives to the "no check"
option, all of which are more useful than nothing in my
opinion. The two that I like are:
1. Check to an arbitrary, user-defined (with a default) but
finite recursion depth. Some Eiffel systems support this
option.
2. A language I helped develop called JJ had two aspects
that supported this feature:
a. visibility of methods in dependent checks impacted
assertion checking --- if a method with wider visibility
called a method (normal or model) with narrower visibility
(e.g., public to private), then then assertion was not
checked. In all other cases (narrow to wide or equal) it was.
b. call trace analysis (track all call traces through the
infrastructure and do cycle detection)
Logged In: YES
user_id=633675
The problem may be that model methods are executing
during the evaluation of some other assertion, hence their
specifications are always disabled.