Issue 18437: Clarify invalid propgation/conformance priority (ocl2-rtf) Source: Model Driven Solutions (Dr. Edward Willink, ed(at)willink.me.uk) Nature: Clarification Severity: Minor Summary: There is a contradiction between invalid conform to anything and invalid always propagates for e.g. Sequence{}->first().oclIsKindOf(Class) oclIsKindOf uses the invalid input to return true. Invalid propagation should dominate giving invalid. This requires OclInvalid::oclIsKindOf, oclIsTypeOf, oclType, oclAsType overloads to explicitly return invalid. Resolution: (A) It is clearly correct that OclVoid/OclInvalid conform to anything so that null/invalid can be used anywhere. (B) It is also clearly correct for navigation on null and invalid to be invalid so that bad results propagate. The above are not contradictory. The contradiction arises through the introduction of the oclIsInvalid() and oclIsUndefined() operations that may be used on null or invalid, despite (B). It would appear that oclIsInvalid() and oclIsUndefined() must be privileged to violate the strictness of (B). If so, are oclIsKindOf, oclIsTypeOf, oclType, oclAsType etc. also privileged? The specification can be clarified by making all oclXXX() operations privileged so that they can be used on null and invalid and defining their OclVoid and OclInvalid overloads explicitly. The affected text can be clarified to eliminate the accidental omission of operation calls for null and invalid. The affected text covers the DataType equality issue so the resolution of Issue 14918 is included Revised Text: In 7.5.11 replace Finally, there is an explicit operation for testing if the value of an expression is undefined. oclIsUndefined() is an operation on OclAny that results in True if its argument is null or invalid and False otherwise. by null objects may be compared with non-invalid objects in = and <> comparisons. Finally, there are explicit operations for testing if the value of an expression is undefined. oclIsUndefined() is an operation on OclAny that results in true if its argument is null or invalid and false otherwise. Similarly oclIsInvalid() is an operation on OclAny that results in true if its argument is invalid and false otherwise. All explicit operations are defined in Clauses 11.3.2 and 11.3.3. In 11.2.3 replace Any property call applied on null results in invalid, except for the oclIsUndefined(), oclIsInvalid(), =(OclAny) and <>(OclAny) operations. by Any operation or property call applied on null results in invalid, except for the oclAsType(), oclIsInState(), oclIsInvalid(), oclIsNew() oclIsUndefined(), oclType(), =(OclAny) and <>(OclAny) operations. In 11.2.4 replace Any property call applied on invalid results in invalid, except for the operations oclIsUndefined() and oclIsInvalid(). by Any operation or property call applied on invalid results in invalid, except for the operations oclIsInvalid(), oclIsUndefined() and oclType(). In 11.3.1 OclAny replace =(object2 : OclAny) : Boolean True if self is the same object as object2. Infix operator. post: result = (self = object2) <> (object2 : OclAny) : Boolean True if self is a different object from object2. Infix operator. post: result = not (self = object2) by =(object2 : OclAny) : Boolean Evaluates to invalid if object2 is invalid. Evaluates to true if self is the same object as object2. Evaluates to true if self and object2 are instances of the same DataType and have the same value. Evaluates to false otherwise. Infix operator. post: result = (self = object2) <> (object2 : OclAny) : Boolean Evaluates to invalid if object2 is invalid. Evaluates to false if self is the same object as object2. Evaluates to false if self and object2 are instances of the same DataType and have the same value. Evaluates to true otherwise. Infix operator. post: result = not (self = object2) In 11.3.2 OclVoid add = (object2 : OclAny) : Boolean Evaluates to invalid if object2 is invalid. Evaluates to true if object2 is the null object. Evaluates to false otherwise. <> (object2 : OclAny) : Boolean Evaluates to invalid if object2 is invalid. Evaluates to false if object2 is the null object. Evaluates to true otherwise. oclAsType(type : Classifier) : T Evaluates to self. oclIsInState(statespec : OclState) : Boolean Evaluates to false. oclIsInvalid() : Boolean Evaluates to false. oclIsKindOf(type : Classifier) : Boolean Evaluates to invalid. oclIsNew() : Boolean Evaluates to false. oclIsTypeOf(type : Classifier) : Boolean Evaluates to invalid. oclIsUndefined() : Boolean Evaluates to true. oclType() : Classifier Evaluates to OclVoid. In 11.3 add (moving 11.3.3 OclMessage to 11.3.4) 11.3.3 OclInvalid = (object : OclAny) : Boolean Evaluates to invalid. <> (object : OclAny) : Boolean Evaluates to invalid. oclAsType(type : Classifier) : T Evaluates to invalid. oclIsInState(statespec : OclState) : Boolean Evaluates to invalid. oclIsInvalid() : Boolean Evaluates to true. oclIsKindOf(type : Classifier) : Boolean Evaluates to invalid. oclIsNew() : Boolean Evaluates to invalid. oclIsTypeOf(type : Classifier) : Boolean Evaluates to invalid. oclIsUndefined() : Boolean Evaluates to true. oclType() : Classifier Evaluates to OclInvalid. Actions taken: February 11, 2013: received issue December 23, 2013: closed issue Discussion: End of Annotations:===== m: webmaster@omg.org Date: 11 Feb 2013 08:58:11 -0500 To: Subject: Issue/Bug Report ******************************************************************************* Name: Edward Willink Employer: mailFrom: ed@willink.me.uk Terms_Agreement: I agree Specification: OCL Section: n/a FormalNumber: 12-01-01 Version: 2.3.1 Doc_Year: 2012 Doc_Month: January Doc_Day: 01 Page: n/a Title: Clarify invalid propgation/conformance priority Nature: Clarification Severity: Minor CODE: 3TMw8 B1: Report Issue Description: There is a contradiction between invalid conform to anything and invalid always propagates for e.g. Sequence{}->first().oclIsKindOf(Class) oclIsKindOf uses the invalid input to return true. Invalid propagation should dominate giving invalid. This requires OclInvalid::oclIsKindOf, oclIsTypeOf, oclType, oclAsType overloads to explicitly return invalid. From: "Brucker, Achim" To: Adolfo Sáhez-Barbudo Herrera , Ed Willink CC: "'ocl2-rtf@omg.org'" Subject: RE: OCL 2.4 Ballot 3 Preview 1 Thread-Topic: OCL 2.4 Ballot 3 Preview 1 Thread-Index: AQHOj2hBizFm600XW0Ow/1DG/9s245mGQ8yAgAPBKgCAA2SO8A== Date: Fri, 9 Aug 2013 21:52:55 +0000 Accept-Language: de-DE, en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [10.21.40.34] X-Virus-Scanned: amavisd-new at omg.org X-MIME-Autoconverted: from quoted-printable to 8bit by amethyst.omg.org id r79Lr2ID014980 Hi, please excuse that I step in late - I was busy with other tasks the last days. > > On the other hand, all these boolean related operators are missing in > the specification for OclVoid and OclInvalid standard library types > (note that issue 18437 resolution from ballot 1 adds other missing > operations). Perhaps we could introduce them along with issue > resolution. > > Finally, and more importantly, my main concern is that we are shifting > from a general rule of doing something on null/invalid yields in > invalid to a very different one which is not entirely justified. The Boolean operations (i.e., the logic of OCL) was always special. Already in OCL 1.3 (and, earlier, the OCL Manifesto) the Boolean operators were an exception to the rule "all operations are strict with respect to 'invalid' (called undefined in at that time). Thus, there core of OCL was a Kleene logic in which the Boolean operators enjoyed the usual algebraic properties such as not (not x) = x or x and y = y and x The latter with the concrete instantiations false and invalid = false and invalid and false = false This is already different from most programming languages in which we would have false and invalid = false and invalid and false = invalid The Kleene approach used by OCL allows for calculi that allow to simplify OCL formulae quite similar to classical logic. We argue that this is a very desirable property for a specification language and, moreover, it allows to build formal reasoning tools for OCL (e.g., as HOL-OCL which is one result of my PhD Thesis). When null was added to OCL, Burkhart and I had many discussions about the the semantics of the logic of OCL with null and invalid. At the end, we agreed that we want to preserve the usual algebraic properties of the Boolean operations to allow for logical reasoning and simplifications over OCL specifications. Thus, we started with the proposition, that not (not x) = x as well as x and y = y and x should hold. The first property already results in the semantics not null = null (if we define 'not null = invalid', we also get 'not (not null) = invalid) Similarly, if we define null and x = invalid This results (from a formal methods / logical point of view) in a very "strange" semantics. The decision to perverse these two basic laws of "not" and "and" fixed, to a large extend, already the semantics of all other Boolean operators (that was one thing we learned when formalizing this semantics in Isabelle/HOL). At least, if we want to preserve the "usual" laws that connect those operators such as x or y = not ((not x) and (not y)) // part of the DeMorgan laws or x xor y = ((not x) and y) or (x and (not y)) Yes, this makes the Boolean operation special as they are an exception to the rule "null.op(...) = invalid". > > "Similarly other logical operations involving null but not invalid > should yield null rather than invalid results. "null and true = null", > "null or false = null", "null xor false = null"." > > Firstly, which is the reasoning behind this ?. Why do we want that > "null xor false" = null rather than invalid ? I hope the reason for this is now clearer. If not, please ask me for further clarifications. I am happy to discuss this in more detail. > > Secondly, this is not true as in proposed resolution, since it looks > like null values dominate invalid values. "null or invalid = null" I would also expect "null or invalid = invalid" similarly to "true or invalid = invalid" (and as we also described in our paper). I will have a detailed look on the resolution over the weekend. Still, I think the resolution is great step in the right direction. Smaller typos can be fixed later in case we cannot fix them immediately. > > Thirdly, this is clashing with other specification statements like in > 11.2.3: > > "Any property call applied on null results in invalid, except > for the oclIsUndefined(), oclIsInvalid(), =(OclAny) and <>(OclAny) > operations". > > or in 11.2.4: > > "Any property call applied on invalid results in invalid, except for > the > operations oclIsUndefined() and oclIsInvalid()." This should, indeed, be fixed. As 'invalid or true = true' was valid since the beginning of OCL, we have this clashes in the standard since quite a while. I hope this helps a little bit. In case of questions, just mail me or ask them on the mailing list. I will happily answer them. And again, please excuse my late reply, I was busy to meet some important deadlines. Regards, Achim -- Dr. Achim D. Brucker, Products & Innovation, SEED Product Security Research SAP AG, Vincenz-Priessnitz-Str. 1, 76131 Karlsruhe, Germany T +49/62 27/7-52595, http://www.brucker.ch, achim.brucker@sap.com Pflichtangaben/Mandatory Disclosure Statements: http://www.sap.com/company/legal/impressum.epx