Invariants evaluating to undefined



Invariants evaluating to undefined

From: Jordi Cabot Sagrera ^lt;jcabot@uoc.edu>
Date: Fri 10 Mar 2006 - 09:18:56 GMT
Message-ID: <2298064.1141982341761.JavaMail.root@costarica>
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
jcabot@uoc.edu
www.lsi.upc.edu/~jcabot
Received on Fri Mar 10 09:19:36 2006