Re: Invariants evaluating to undefined



Re: Invariants evaluating to undefined

From: Thomas Baar ^lt;thomas.baar@epfl.ch>
Date: Fri 10 Mar 2006 - 12:58:29 GMT
Message-ID: <441177F5.90902@epfl.ch>
Hi Jordi,

your understanding of OCL is correct.

>Dear all,
>
>I have some questions regarding the behavior of invariants when its
>body evaluates to an undefined result. According to the OCL standard
>“A system state is called valid with respect to an invariant if the
>invariant evaluates to true. Invariants with undefined result
>invalidate a system state”. 
>
>Surprisingly (at least for me) this is not the common approach taken
>in the database field, where a system state is valid with respect to
>an invariant when the invariant does not evaluate to false (i.e. it
>may evaluate to true or undefined). Is there any particular reason
>to consider that states evaluating an invariant to undefined are not
>valid? Can you point me some work on this topic?
>  
>
At this puml list we had already quite few discussions on undefined but
didn't come to an general conclusion (at least that was my perception).

Evaluating an expression to undefined can have different kind of sources
and it would be worthwhile, to distinguish between these kinds more 
carefully
in the OCL. One possibility is that the evaluation of expressions with
pre-defined main functor fails, e.g. incomePerPerson = bugdet / 
self.person->size()
If there are no persons linked to self, then the right-hand side of the
equation would be a division by zero. It might be a matter of taste but
OCL refuses this equation to be a valid invariant as long as the size
of linked persons is 0. I support this viewpoint since it helps to detect
some unclear issues of the OCL specification and urges the specification
author to be more precise here. The unclear issue could be resolved easily
by applying the same technique as in your example:
self.person->notEmpty() implies incomePerPerson = bugdet / 
self.person->size()

>Moreover, I have some doubts about when an ocl expression evaluates
>to undefined. Assume that we have two classes (Department and
>Person) related with the association Manages (departments can be
>managed by 0..1 Person). Then an invariant stating that the salary
>of the manager must be lower than the maxSalary defined in the
>department could not be written this way:
>  
>  context Department inv: self.maxSalaryDept > self.person.salary 
>
>since then, system states having departments without managers would
>evaluate the invariant to undefined (am I right?), and thus, they
>would be considered invalid (although the cardinality of the Manages
>association admits departments without managers)
>  
>
In your example, the undefinedness results from a navigation over a
non-existing link. Again, OCL's opinion is that at 'run-time' all 
navigations
that are used in the OCL constraint must be possible. If not, we run
into a 'problematic situation' and this is better resolved by the 
specification author.

>We should change the invariant to the more verbose one:
>
>   context Department inv: self.person->notEmpty() implies    
>                           self.maxSalaryDept > self.person.salary 
>
>Curiously, when changing the cardinality to 0..* (a department can
>have several managers) I think the following invariant is already
>correct:
>
>context Department inv: 
>   self.person->forAll(salary < self.maxSalaryDept)
>
>we don’t need to check that self.person is not empty since I think
>the forAll iterator over an empty set returns true so deparments
>without managers do not invalidate now a system state (again, I may
>be wrong). To me, it seems a little strange to have to check or not
>the emptiness of the navigation depending on the maximum
>multiplicity of the association.
>  
>
The forAll is defined in OCL as in classic logic. It is nothing suspicious
to evaluate a forAll-expression always to true when applied on an
empty collection. For instance, would you call me a liar if I would say
that all my Daimlers are of color 'red'. I don't have a Daimler (not 
even a car),
so my claim that all my Daimlers are red is ok, isn't it?

Btw, your forAll-version of the invariant also works if you keep 0..1 as
the multiplicity of the association end.

Best regards,
Thomas


-- 
Dr. Thomas Baar
Software Engineering Laboratory
School of Computer and Communication Sciences EPFL
EPFL IC UP-LGL
INJ 337 (Bâtiment INJ)
Station 14
CH-1015 Lausanne, Switzerland
Tel +41 21 693 2580, Fax +41 21 693 5079
mailto:thomas.baar@epfl.ch   http://lgl.epfl.ch/members/baar/
********************************************************
Do not miss MoDELS/UML 2006: see http://www.modelsconference.org for the 9th International Conference on Model Driven Engineering Languages and Systems (formerly the UML series of conferences)
Received on Fri Mar 10 12:59:02 2006