Re: asking about OCL



Re: asking about OCL

From: Prof. Dr. Peter H. Schmitt <pschmitt_at_ira.uka.de>
Date: Wed, 17 May 2006 13:25:56 +0200
Message-ID: <446B0844.3090703@ira.uka.de>
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
formulation:

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.

regards

Peter

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.
> 


-- 
Prof.Dr.P.H.Schmitt
Fakultät für Informatik
Universität Karlsruhe
Received on Wed 17 May 2006 - 12:26:15 BST