RE: Invariants evaluating to undefined

RE: Invariants evaluating to undefined

From: D H. Akehurst ^lt;>
Date: Fri 10 Mar 2006 - 12:18:52 GMT
Message-ID: <>
You can use the invariant

context Department inv: 
   self.person->forAll(salary < self.maxSalaryDept)

In the case where the multiplicity is [0..1].

Using the '->' operator on objects that are not collections automatically wraps
the object in a Set.

Wraping an undefined value into a set results in an empty set, hence your expression
gives true when there are no managers.

Hope this helps.

> -----Original Message-----
> From: 
> [] On Behalf Of Jordi 
> Cabot Sagrera
> Sent: 10 March 2006 09:19
> To:
> Subject: Invariants evaluating to undefined
> 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?
> 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)
> 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.
> Any comments will be really appreciated!
> Jordi
> Cordialment,
> Jordi Cabot Sagrera
> Professor dels Estudis d'Informātica i Multimčdia
> Universitat Oberta de Catalunya
Received on Fri Mar 10 12:19:32 2006