Re: Invariants evaluating to undefined



Re: Invariants evaluating to undefined

From: D H. Akehurst ^lt;D.H.Akehurst@kent.ac.uk>
Date: Mon 13 Mar 2006 - 08:13:02 GMT
Message-ID: <A97ADB9E8A23214492A613C7EC1CAF7B3C0B30@dogsbody.ee.kent.ac.uk>
The  'Set{undefined} = Set{} ' issue is not a "proposal".
 
It was our interpretation of the information given in the standard. It
was the only interpretation we found to be consistent with 
"prop->isEmpty() = prop.oclIsUndefined()"
 
I have just looked at the June 2005 version of the standard,
 
in this there is explicit discussion of 'null' values, and their
containment in collections [section 8.2].
 
I have to say that I don't know if this is the latest version of the
standard, just the latest I could find on OMG web site.
 
I also don't really understand the new introduction of 'OclInvalid' Why
is this needed/different to OclUndefined ??


________________________________

	From: Dan CHIOREAN [mailto:chiorean_d2001@yahoo.com] 
	Sent: 11 March 2006 09:26
	To: jcabot@uoc.edu; D H. Akehurst; thomas.baar@epfl.ch;
sz9@inf.tu-dresden.de; france@CS.ColoState.EDU; pschmitt@ira.uka.de;
dnj@mit.edu; puml-list@cs.york.ac.uk
	Subject: Re: Invariants evaluating to undefined
	
	
	Dear all,
	
	OCL was conceived as a complementar formalism for the visual
one, used in modeling languages.  Therefore, even in cases of the most
simple models, like the model proposed by Jordi, representing the class
diagram is more that a wise attitude, it is mandatory.
	
	OCL specifications must be as comprehensible and unambigous as
possible.  In Jordi's example, the apropriate invariant is:
	
	context Company
	   inv maxSalaryDept:
	      (not self.manager.oclIsUndefined) implies
(self.maxSalaryDept > self.manager.salary)
	
	This specification is more suggestive that
self.manager->isEmpty.  Using the oclIsUndefined operation, it is very
clear that a department may have at most one manager not a collection of
managers.
	
	In models, collections are obtained by navigating multiple
associations.  The "->" operator can be used exclusively on collections.
My oppinion is that using the ".property" expression instead of
"->collect(property)" was not the best decision in the OCL language.
	
	Doing "automatic conversions" from an element to a collection of
elements is unacceptable; Element <> Collection(Element) - OCL is a
typed language.  Dave's proposal to consider Set{undefined} = Set{} may
lead to absurd situations.
	
	Let consider the following case:  A Department may have at most
one manager and two spokesmen.  Both the manager and the spokesmen are
persons and the class Person has an attribute name.  Supose that at a
moment, the Department has a manager and has not spokesmen.  The
manager's name is unknown at (for) that moment.
	
	Conforming to Dave's proposal, the expresion defined in the
Department context:
	
	context Department
	
	self.manager.name = self.spokesmen.name, would be evaluated to
Set{undefined} = Set{}, resulting true. :((
	
	In the following I would like to discuss other aspects related
to Jordi's question.
	
	In the DepartmentPerson model, maxSalaryDept, is not an
apropriate invariant for the Department context because it depends on
salary, an attribute specified in the class Person.
	
	In the wellknown CompanyExample model (used in all OCL
specifications), salary is natural modeled as an attribute of the
associationClass Job.  My oppinion is that in Jordi's problem, the
natural solution is to specify a precondition for the
addNewJob(p:Person, j:Job):Set(Job) operation, specified in the
Department class.  In case of an updateSalary(ns:Integer) operation,
specified in the class Job, a similar precondition will be required.
	
	Please find attached an archive containing some models and
different OCL specifications realized using OCLE.  The specifications
may be evaluated on different snapshots.
	
	Best regards,
	
	Dan Chiorean 

	
________________________________

	Yahoo! Mail
	Bring photos to life! New PhotoMail
<http://pa.yahoo.com/*http://us.rd.yahoo.com/evt=39174/*http://photomail
.mail.yahoo.com> makes sharing a breeze. 
Received on Mon Mar 13 08:13:47 2006