search

eclipse-ocl / org.eclipse.ocl

Eclipse Public License 2.0
0 stars 0 forks source link

[evaluator] pre and post conditions are ignored #520

Closed eclipse-ocl-bot closed 1 month ago

eclipse-ocl-bot commented 1 month ago

| --- | --- | | Bugzilla Link | 303686 | | Status | RESOLVED DUPLICATE of bug 520440 | | Importance | P3 normal | | Reported | Feb 23, 2010 15:19 EDT | | Modified | Apr 28, 2021 03:58 EDT | | Version | 3.0.0 | | Blocks | 318358 | | Reporter | Ed Willink |

Description

There should be an option/compulsion to evaluate pre and post-conditions.

eclipse-ocl-bot commented 1 month ago

By Ed Willink on Mar 14, 2011 16:44

Bug 337877 has been marked as a duplicate of this bug.

eclipse-ocl-bot commented 1 month ago

By Ed Willink on May 01, 2011 06:17

Finally: a use case from news://new.eclipse.org:119/ipj32b$p3t$1@news.eclipse.org.

Allow pre-conditions to be evaluated by a GUI so that the applicability of some GUI operation can be determined before the model is broken and an invariant violated.

eclipse-ocl-bot commented 1 month ago

By Ed Willink on Apr 28, 2021 03:58

The symbolic Validity Analysis for Bug 520440 probably resolves all of this and more.

Normally there is no point evaluating a precondition at run-time since it just burns time predicting and then crashing as a prefix to the actual code that will crash anyway.

Many postconditions are executale and so differ little from bodyCondition/bodyEpressions. However for e.g. sort() a post-condition may be much simpler than the quiksort implementation.

Most explicit and implicit preconditions are exactly what is needed to allow a compile time validity analysis to diagnose all unjustified crashes. Invariants and postconditions can provide further assistance. There is no need to execute pre/post at run-time. Confirming the compatibility of a complex body with its postconditions is perhaps something for a proof tool.

(In reply to Ed Willink from comment #2)

Finally: a use case from news://new.eclipse.org:119/ipj32b$p3t$1@news.eclipse.org.

Unfortunately this link is dead. Attempting to find it on the FUDForum is not clearly successful. 2011 was very early in the support for OCL editors and so the comments on GUI may be no more than 'live validation' rather than some dynamic UI installer.

This bug has been marked as a duplicate of bug 520440