RE: Re: Invariants evaluating to undefined



RE: Re: Invariants evaluating to undefined

From: Jordi Cabot Sagrera ^lt;jcabot@uoc.edu>
Date: Mon 13 Mar 2006 - 14:04:07 GMT
Message-ID: <357720.1142258671312.JavaMail.root@bermudas>
Dear all,

Thanks for all your responses. They have helped me to understand 
some of the "obscured" semantics of the OCL (although it seems 
that there is not yet a complete consensus on some of them).

Just two remarks about Dan’s contribution:

- You can always express the constraints not as invariants but as 
operation preconditions. However, this is an error-prone task (a 
designer may add the corresponding precondition to the addNewJob 
operation but forget about adding also the precondition to other 
conflictive operations as updateSalary). That is way I prefer to 
specify constraints as invariants instead of using preconditions 
whenever possible. 

- “maxSalaryDept, is not an appropriate invariant for the 
Department context because it depends on  salary, an attribute 
specified in the class Person” -> In my opinion there is not a 
best context to define an invariant, at least from a code-
generation point of view (i.e. when generating the code to verify 
a constraint we may need to redefine the constraint in terms of 
different contexts to get an optimal result). I agree that, from a 
simplicity point of view, an invariant may become simpler 
depending on the context type used to express it. 

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 Mon Mar 13 14:05:05 2006