Re: asking about OCL

Re: asking about OCL

From: Prof. Dr. Peter H. Schmitt <>
Date: Wed, 17 May 2006 13:25:56 +0200
Message-ID: <>
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

context A
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:
> Hi,
> 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
Universität Karlsruhe
Received on Wed 17 May 2006 - 12:26:15 BST