Re: asking about OCL
We also came across this problem. But, it turned out that
in our context the solution was trivial. I suggest to
adopt the same position for OCL.
An invariant is understood as a formula in the input language
to our prover. All free variables occuring implicitly or explicitly
are universally quantified, as the OCL standard requires. If the
invariant does not contain a variable, as is the case for the static
invariant A::allInstances() -> ...
this universal quantification has not effect.
So there is nothing wrong with Frédéric FONDEMENT's
inv testExistence: A::allInstances()->notEmpty()
You may also want to check how the JML community deals with this.
They distinguish static invariants from instance invariants.
Steffen Zschaler wrote:
> That's a very good question indeed. I think, what you are saying is that
> the 'inv' context is not well chosen for this kind of constraint,
> because it always has the implicit all-quantification.
Fakultät für Informatik
Received on Wed 17 May 2006 - 12:26:15 BST