Open eclipse-ocl-bot opened 1 month ago
By Ed Willink on Mar 15, 2013 07:10
It shouldn't be necessary for a user to refactor at all.
Constraints such as:\ inv A: ...\ inv B: ...\ inv C: ...
can be evaluated as (A and B and C) so that common sub-expression elimination hoists shared terms. It is only necessary to annotate the nested terms that correspond to explicit invariants to ensure that error reports reflect the user perspective.
By Ed Willink on Jun 07, 2020 13:11
This suggestion should also be searchable as a callable constraint / inavariant.
In Bug 544629#c8 The symbolic evaluator needs to pull in an invariant to provide some extra truth to avoid the symbolic validation failing.
An invariant may therefore be invoked as a true-valued-function in any function.
By Ed Willink on Jun 07, 2020 13:19
(In reply to Ed Willink from comment #2)
An invariant may therefore be invoked as a true-valued-function in any function.
But as a cached Boolean-valued prerequisite from any invariant.
CG/evaluation options could enable:
| --- | --- | | Bugzilla Link | 401786 | | Status | NEW | | Importance | P3 enhancement | | Reported | Feb 26, 2013 08:31 EDT | | Modified | Jun 07, 2020 13:19 EDT | | Reporter | Ed Willink |
Description
Given constraints written as:
def checkSimpleConstraint() : Boolean = ...\ inv SimpleConstraint: checkSimpleConstraint()\ inv ComplexConstraint: checkSimpleConstraint() implies ...
the constraint evaluation should recognise that SimpleConstraint guard ComplexConstraint and avoid calling checkSimpleConstraint() twice.