Issue 9796: Section: 7.3.4 (ocl2-rtf) Source: (, ) Nature: Clarification Severity: Minor Summary: We consider a Sequence of instances of a class called 'Example'. This class has an integer attribute called 'ex'. If we have a method specification written as follow: pre: datalist->isTypeOf(Sequence(Example)) post: Sequence{1..datalist->size()}->forAll(n | datalist->at(n).ex = datalist@pre->at(n).ex) I not sure if is correct writes the same specification with the next sentences: pre: datalist->isTypeOf(Sequence(Example)) post: datalist->forAll(n | n.ex = n@pre.ex) The generic questions is: What does the '@pre' operator mean when it is applied to iterators variables (as 'n' in the example)? Is correct the @pre use in this cases? I hope you understand my dude and sorry any gramatical error because my written english is very poor. Resolution: Revised Text: Rewrite Section 7.5.14 as follows, using “feature” instead of “property” to include operations and “behavior” instead of “method” to include more than just those behaviors that are the methods of operations: 7.5.14 Previous Values in Postconditions As stated in Section 7.3.4, “Pre- and Postconditions,” on page 8, OCL can be used to specify pre- and postconditions on operations and behaviors in UML. In a postcondition, the expression can refer to values of any feature of an object at two moments in time: the value of a feature at the start of the operation or behavior the value of a feature upon completion of the operation or behavior The value of an operation call or a property navigation in a postcondition is the value upon completion of the operation. To refer to the value of the feature at the start of the operation, one has to postfix the property name with the keyword ‘@pre’: context Person::birthdayHappens() post: age = age@pre + 1 The property age refers to the property of the instance of Person that executes the operation. The property age@pre refers to the value of the property age of the Person that executes the operation, at the start of the operation. In the case of an operation call, the ‘@pre’ is postfixed to the operation name, before the parameters. context Company::hireEmployee(p : Person) post: employees = employees@pre->including(p) and stockprice() = stockprice@pre() + 10 When the pre-value of a feature evaluates to an object, all further properties that are accessed of this object are the new values (upon completion of the operation) of this object. So: a.b@pre.c -- takes the old value of property b of a, say x -- and then the new value of c of x. a.b@pre.c@pre -- takes the old value of property b of a, say x -- and then the old value of c of x. The ‘@pre’ postfix is allowed only in OCL expressions that are part of a Postcondition, and only on invocations of the features of model classifiers. Asking for a current property of an object that has been destroyed during execution of the operation results in null. Also, referring to the previous value of an object that has been created during execution of the operation results in null. In Section 8.3.1 Expressions Core, add a property to the FeatureCallExp metaclass: FeatureCallExp A FeatureCallExp expression is an expression that refers to a feature that is defined for a Classifier in the UML model to which this expression is attached. Its result value is the evaluation of the corresponding feature. Attributes isPre Boolean indicating whether the expression accesses the precondition-time value of the referred feature. Figure 8.3 is updated to show an “isPre : Boolean” attribute in the FeatureCallExp metaclass. In Section 8.3.9 Additional Operations on OCL Metaclasses, subsection OclExpression, the definition of the withAtPre() operation is deleted. In Section 9.3 Concrete Syntax, the Synthesized Attributes of the OperationCallExpCS are updated to utilize the FeatureCallExp::isPre attribute: [E] -- indicate the precondition-time value OperationCallExpCS.ast.referredOperation = OclExpressionCS.ast.type.lookupOperation (simpleNameCS.ast, if argumentsCS->notEmpty() then arguments.ast->collect(type) else Sequence{} endif) OperationCallExpCS.ast.arguments = argumentsCS.ast OperationCallExpCS.ast.isPre = true [F] -- indicate the precondition-time value with the implicit source OperationCallExpCS.ast.arguments = argumentsCS.ast and OperationCallExpCS.ast.referredOperation = env.lookupImplicitOperation(simpleName.ast, if argumentsCS->notEmpty() then arguments.ast->collect(type) else Sequence{} endif) ) OperationCallExpCS.ast.isPre = true In Section 9.3 Concrete Syntax, the occurrences of PropertyCallExpCS are changed to CallExpCS as was the AbstractSyntax. In Section 9.3 Concrete Syntax, the occurrences of ModelPropertyCallExpCS are changed to FeatureCallExpCS as was the AbstractSyntax. In Section 9.3 Concrete Syntax, the occurrences of AttributeCallExpCS are changed to PropertyCallExpCS as was the AbstractSyntax. In Section 9.3 Concrete Syntax, the definition of AttributeCallExpCS is updated with Property terminology as was the Abstract Syntax. It also utilizes the FeatureCallExp::isPre attribute: PropertyCallExpCS This production rule results in a PropertyCallExp. In production [A] the source is explicit, while production [B] is used for an implicit source. Alternative [C] covers the use of a static attribute. [A] PropertyCallExpCS ::= OclExpressionCS ‘.’ simpleNameCS isMarkedPreCS? [B] PropertyCallExpCS ::= simpleNameCS isMarkedPreCS? [C] PropertyCallExpCS ::= pathNameCS Abstract syntax mapping PropertyCallExpCS.ast : PropertyCallExp Synthesized attributes [A] PropertyCallExpCS.ast.referredProperty = OclExpressionCS.ast.type.lookupAttribute(simpleNameCS.ast) [A] PropertyCallExpCS.ast.source = OclExpressionCS.ast [A] PropertyCallExpCS.ast.isPre = isMapkedPreCS->notEmpty() [B] PropertyCallExpCS.ast.referredProperty = env.lookupImplicitAttribute(simpleNameCS.ast) [B] PropertyCallExpCS.ast.source = env.findImplicitSourceForProperty(simpleNameCS.ast) [B] PropertyCallExpCS.ast.isPre = isMarkedPreCS->notEmpty() [C] PropertyCallExpCS.ast.referredProperty = env.lookupPathName(pathNameCS.ast).oclAsType(Property) Inherited attributes [A] OclExpressionCS.env = PropertyCallExpCS.env Disambiguating rules [1] [A, B] ‘simpleName’ is name of a Property of the type of source or if source is empty the name of an attribute of ‘self’ or any of the iterator variables in (nested) scope. In OCL: not PropertyCallExpCS.ast.referredProperty.oclIsUndefined() [2] [C] The pathName refers to a class attribute. env.lookupPathName(pathNameCS.ast).oclIsKindOf(Property) and PropertyCallExpCS.ast.referredProperty.ownerscope = ScopeKind::instance NavigationCallExpCS This production rule represents a navigation call expression. [A] NavigationCallExpCS ::= PropertyCallExpCS [B] NavigationCallExpCS ::= AssociationClassCallExpCS Abstract syntax mapping NavigationCallExpCS.ast : NavigationCallExp Synthesized attributes The value of this production is the value of its child production. [A] NavigationCallExpCS.ast = PropertyCallExpCS.ast [B] NavigationCallExpCS.ast = AssociationClassCallExpCS.ast Inherited attributes [A] PropertyCallExpCS.env = NavigationCallExpCS.env [B] AssociationCl assCallExpCS.env = NavigationCallExpCS.env Disambiguating rules These are defined in the children. In Section 9.3 Concrete Syntax, the AssociationEndCallExpCS subsection and its subsubsections are deleted, as UML 2.x merges the Attribute and AssociationEnd constructs in a single Property metaclass. In Section 9.3 Concrete Syntax, the Synthesized Attributes of the AssociationClassCallExp subsection are updated to utilize the FeatureCallExp::isPre attribute: [A] AssociationClassCallExpCS.ast.referredAssociationClass = OclExpressionCS.ast.type.lookupAssociationClass(simpleNameCS.ast) AssociationClassCallExpCS.ast.source = OclExpressionCS.ast AssociationClassCallExpCS.ast.isPre = isMarkedPreCS->notEmpty() [A] AssociationClassCallExpCS.ast.qualifiers = argumentsCS.ast [B] AssociationClassCallExpCS.ast.referredAssociationClass = env.lookupImplicitAssociationClass(simpleNameCS.ast) AssociationClassCallExpCS.ast.source = env.findImplicitSourceForAssociationClass(simpleNameCS.ast) AssociationClassCallExpCS.ast = isMarkedPreCS->notEmpty() [B] AssociationClassCallExpCS.ast.qualifiers = argumentsCS.ast Actions taken: May 27, 2006: received issue October 16, 2009: closed issue Discussion: The usage of @pre is only applicable to the features of model classifiers, as indicated in Section 7.5.14 (Previous Values in Postconditions) which identifies both attributes and operations as “properties”, and in Definition A.31 (Syntax of Expressions in Postconditions) in which it is stated that @pre may be applied to operations that depend on system state, such as operation calls and attribute navigation on objects. The Abstract Syntax Model is ambiguous in the model of expressions involving @pre. It only defines an additional operation on the OclExpression metaclass that serves as a factory for OperationCallExps that represent invocations of an atPre() operation. This atPre() operation in not defined, neither in the Standard Library nor as an additional operation, itself. This proposed resolution is clearer, more concise, and simpler. It also does not pre-suppose a mechanism by which evaluation of @pre expressions may be accomplished End of Annotations:===== m: webmaster@omg.org Date: 27 May 2006 11:35:06 -0400 To: Subject: Issue/Bug Report -------------------------------------------------------------------------------- Name: Jorge Bejar Company: none mailFrom: jmbejar@gmail.com Notification: Yes Specification: OCL 2.0 Specification Section: 7.3.4 FormalNumber: ptc/2005-06-06 Version: 2.0 RevisionDate: 06-06-2005 Page: 24 Nature: Clarification Severity: Minor HTTP User Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.7.12) Gecko/20050915 Firefox/1.0.7 Description We consider a Sequence of instances of a class called 'Example'. This class has an integer attribute called 'ex'. If we have a method specification written as follow: pre: datalist->isTypeOf(Sequence(Example)) post: Sequence{1..datalist->size()}->forAll(n | datalist->at(n).ex = datalist@pre->at(n).ex) I not sure if is correct writes the same specification with the next sentences: pre: datalist->isTypeOf(Sequence(Example)) post: datalist->forAll(n | n.ex = n@pre.ex) The generic questions is: What does the '@pre' operator mean when it is applied to iterators variables (as 'n' in the example)? Is correct the @pre use in this cases? I hope you understand my dude and sorry any gramatical error because my written english is very poor.