The use of explicit null and invalid values in OCL can lead to complex and hard-to-verify specifications. In addition, these values complicate the logic of OCL and of transformation languages that use OCL, making it difficult to provide effective verification support for these languages. We define an alternative technique for using OCL with UML and model transformations which avoids the use of null and undefined values, and we present verification techniques for a transformation language, UML-RSDS, based on this approach.
OCL is the official textual specification language used with the UML, and it is also widely used as a constraint language within model transformation languages, such as ATL, QVT, ETL, Kermeta and others to define transformation rules, although each of these languages tend to adopt variations with the OCL standard. For example, Kermeta uses the keyword void for the null value, and ETL uses isDe ned () instead of oclIsUnde ned () in its variant OCL, EOL.
The OCL standard [
The principal reason why null arises in UML and OCL is the need to represent the value of optional association ends (e.g., Figure 1): if a person has no spouse, this is expressed by spouse = null . An attempt to evaluate a feature of a null object results in invalid , however null is treated as being Bag {} when a collection operation is applied to it. Thus spouse.age is undefined if spouse is null , but spouse→collect (age) is Bag {}, contradicting the usual expectation that these expressions should have the same value.
Null values can also be returned by operations, and this leads to a problem which OCL shares with object-oriented programming languages: that programmers may return null from an operation to indicate that it has failed, instead of using exceptions or other error-handing facilities. For example an operation to marry two Person objects could return null if the operation cannot be successfully completed, but this does not inform the caller why the operation failed: it can fail for several different reasons.
The explicit use of null therefore complicates system specification and
verification by introducing undefinedness into expressions and by encouraging the
use of hard-to-verify specification styles. It also has a direct impact on the use
of verification tools by complicating the logic used for reasoning about systems
and models. The truth tables for each logical operator not , and , or , xor and
implies of OCL must incorporate cases for null , for example:
null and null
false and null
true and null
null and false
null and true
=
=
=
=
=
null
false
null
false
null
null acts as an unspecified or ‘unknown’ element in these tables, resulting in
a 3-valued logic [
Even within the UML standards there remain unclear issues with the
semantics of null and invalid , for example, whether an allInstances() collection
can contain an undefined element, or whether null .oclIsKindOf (A) should
return true/false or invalid (http://www.omg.org/issues/ocl2-rtf.open.html).
Languages based on OCL often adopt variant semantics to the standard. For
example, whilst OCL permits null elements in collections, in QVT-O assignments null
elements in collections are ignored (Section 8.2.2.11 of [
This lack of clear semantics for null and invalid means that tools which
do attempt to handle full OCL necessarily make specific assumptions about
the semantics, which may not match the specifier’s intentions. For example, in
order to formally model null and invalid in HOL, [
We consider that this lack of a clear semantics, and the variability of definitions in different MT languages is an indication that the use of explicit null and unde ned elements is unsuited to situations where formal verification of model transformations is required.
In this paper we propose an alternative approach for the use of OCL and related constraint languages in model transformation specifications, in accordance with the following principles: (1) Transformation specifications should use expressions which are ensured by their context to be well-defined (not null or invalid ) and determinate in value. null or invalid values should not be used. (2) Expressions which are used as conditional tests or pure values should be non-side-effecting.
These principles greatly facilitate analysis and verification of model transformations, by ensuring that expressions can be given consistent meanings in (i) the transformation language; (ii) in formal languages used to analyse the transformation, and (iii) in programming languages used to implement the transformation.
In Section 2 we describe our proposed alternative to standard OCL, in Section 3 we describe how it can be used for transformation specification, and in Section 4 describe transformation verification based on alternative OCL. 2
In order to generally resolve the difficulties caused by explicit null and invalid
values, we have developed and applied an alternative OCL-like formalism, which
retains most of the notation and concepts of OCL, but which has no null or
invalid elements, and is based on classical 2-valued logic and set theory.
Transformation specifiers should ensure that invalid expression evaluations cannot
occur in their transformations, using the definedness conditions of expressions
(Table 1). In cases where operators can produce invalid evaluations, additional
operators are provided to test for validity before the evaluation is attempted.
Eg., for toInteger () on String we provide an operation isInteger () to check that
a string represents a valid integer before attempting to convert it [
Side-effects are only permitted for expressions which are calls obj .op(e) of update (non-query) operations op. Expressions should not have side-effects when used as conditions or pure values. Together with the restriction that undefined values cannot occur, this leads to the same logic for the logical connectives both in OCL and in the formal and programming languages which we treat (B AMN, Java, C# and C++): in programming languages ‘short-circuit’ evaluation is used to determine that P and Q is false if P is false, without the need to evaluate Q . This is semantically equivalent to an ‘evaluate all arguments completely’ semantics if undefined values and side effects are prohibited.
We use some minor extensions of OCL. For entity types E with one attribute id designated as an identity attribute (primary key), the abbreviation E [v ] is introduced to represent the standard OCL expression E .allInstances()→any (id = v ), if v is single-valued, and to represent E .allInstances ()→select (v →includes(id )) if v is collection-valued. For an instance-scope attribute att of E , E .att denotes E .allInstances ()→collect (att ).
Examples of the clauses for the definedness function def : Exp(L) → Exp(L) are given in Table 1. Expression determinacy det : Exp(L) → Exp(L) can be similarly defined.
De nedness condition def(e) b ̸= 0 and def (a) and def (b) def (e) and E :allInstances()→includes(e) where E is the declared classifier of e def (e) and E :allInstances()→includes(e) and def (p) and def (e:Postop(p)) where E is the declared classifier of e, Postop the postcondition of op ind > 0 and ind ≤ s→size() and def (s) and def (ind )
E :id →includes(v ) and def (v ) Constraint expression e a=b e:f Data feature application Operation call e:op(p) s→at(ind ) sequence, string s E [v ] entity type E with identity attribute id , v single-valued A and B A implies B str :toInteger () str :toReal () obj :oclAsType(E ) def (A) and def (B ) def (A) and (A implies def (B )) def (str ) and str :isInteger () def (str ) and str :isReal () def (obj ) and obj :oclIsKindOf (E )
Table 1. Definedness conditions for expressions Inductive proof of definedness may be needed for recursive operation calls.
The main difference between our constraint language and standard OCL is that optional association ends are treated as being collections of size 0 or 1, rather than being null or a single defined object. This interpretation is consistent with the use of multiplicity bounds for other many-valued association ends, and is also already adopted in OCL in the case that collection operators are applied to the optional association end (because of the implicit casting of null to Bag {} in such cases). The test spouse→isEmpty () can then be used in place of spouse.oclIsUnde ned (), and spouse→any (true) returns the Person object if spouse is non-empty.
This approach has several advantages: { Classical logic can be used in reasoning, there is no need for null and invalid . { It is simple to evolve a model using a 0..1 multiplicity association end to one with a 0..n or * multiplicity, and vice-versa, since the association end remains a collection. { Collections cannot contain null elements, simplifying their processing, both in OCL and in programs synthesised from the OCL.
In our alternative OCL semantics there is no null element, however there are ‘unallocated object references’. There is a fixed denumerable type Object OBJ of possible object references, a finite set objects ⊆ Object OBJ of object references of existing objects, and for each class or interface E in a UML class diagram, a finite set, E .allInstances() ⊆ objects, of the references that refer to actually existing E objects. Creation of an E instance selects an element ex from Object OBJ − objects, adds it to E .allInstances (), objects and to all superclass instance sets of E , and allocates an object for ex , including values for all features of E (including inherited features). On deletion ex →isDeleted (), the reverse process applies, and ex is returned to the set of available object references. It is removed from any association end or other collection in the system. It is a semantic error to refer again to ex after it has been deleted.
Applying our approach to the red-black tree specification of [
color implies left →forAll (not color ) and right →forAll (not color ) in comparison to
color implies ((left = null or not left .color ) and (right = null or not right .color ))
in [
OCL was originally intended as a language for logical expression evaluation, to express declarative constraints of UML models. However, transformation languages such as QVT and Kermeta now use OCL to define executable effects, to update models. The imperative use of OCL as a programming language introduces semantic problems, for example, how a forAll or other iteration should behave if (logically) its evaluation can be terminated before all elements are processed, whilst (imperatively) some intended side-effect behaviour could still arise if additional elements are considered. Failing to evaluate all of the quantified collection would also violate the requirement that the expression should evaluate to invalid if any of its individual element evaluations do.
We rule out such cases by clearly distinguishing the logical and imperative use
of OCL. A function stat gives an imperative denotation of certain expressions as
statements (activities). This defines precisely when an expression e is interpreted
imperatively, i.e., as an activity stat (e) [
For example, logical evaluation of s→forAll (x | x .att = v ) can return false as soon as some x ∈ s with x .att ̸= v is found, and no updates are performed. But stat (s→forAll (x | x .att = v )) is for x : s do x .att := v and always iterates completely through all elements of s, assigning v to x .att for each x ∈ s. The logical and imperative interpretations are related naturally by the property def (e) ⇒ [stat (e)]e where [ ] is the weakest-precondition operator on activities. 3
The alternative OCL described in the preceding section can be used to define
model transformations at a declarative level. In UML-RSDS [
The typical form of a postcondition Cn in Cons is an implication constraint Ante implies Succ on a context entity type ST belonging to the source language S of τ . This represents a declarative assertion that, at termination of the transformation, for each instance self of ST which satisfies Ante, Succ also holds. The definedness condition def (Cn) from Table 1 is
def (Ante) and (Ante implies def (Succ)) so that the context ST of Cn must ensure that Ante is defined, and that Ante ensures definedness of Succ. The succedent should normally have an imperative denotation stat (Succ). The definedness of each constraint in Cons is a proof obligation which the transformation specifier should establish. Asm and preceding postconditions can be used as assumptions for the definedness obligations. These obligations can be submitted to a proof tool. Likewise, the determinacy condition det (Cn) of each postcondition should normally be established for the specification, and specifiers should ensure that no update (non-query) operation is invoked in any Ante condition or other conditional test/value expression in any Cn. Whilst these obligations are additional proof burdens for the developer, they can help to identify errors in the specification, and provide assurance of correctness.
For separate-models transformations, ST and other source model data are not modified by τ , instead instances of target language entity types are created and their features defined. A typical postcondition constraint for this kind of transformation has the form
Ante implies TT →exists (t | Succ1) which specifies that corresponding target model instances t of target entity type TT should exist for each source model instance self of ST that satisfies Ante. Succ1 can define the feature values of t based upon those of self (or on any other source or target model data).
Executable code in Java, C# and C++ can be generated for transformations (or for general software systems) from UML-RSDS specifications. A postcondition constraint Cn is implemented by stat (Cn), and this activity serves as an intermediate representation from which program code in specific programming languages can be generated. A guarantee is given that no collection in the executable program can ever contain null objects. In addition, when an object a of class C is explicitly deleted (by the expression a→isDeleted ()), then it is also removed from any collection in the system (objects b with a 1-multiplicity association end with value a are deleted along with a), so removing the possibility of ‘dangling references’.
UML-RSDS has been successfully used for a large number of transformation
problems, including industrial case studies. For example, it was used in the
comparative case study of [
As an example of UML-RSDS specification, Figure 2 shows the metamodels of a UML to relational database transformation which maps root classes to tables, and attributes to columns of the table of the root class of their class. p : ownedAttribute and t = Table[rootClass().name] implies
Column->exists( cl | cl.name = p.name and cl : t.tcols ) This adds, for each attribute p of self , a column cl to the table t corresponding to the root class of self . rootClass is an auxiliary query operation of Entity defined as: rootClass( ) : Entity post: ( superclass.size = 0 implies result = self ) and ( superclass.size > 0 implies
result = superclass.rootClass()->any(true) )
To prove def (C 2) requires proof that the call to rootClass is well-defined, which follows from Asm, and then that Table[rootClass().name] is well-defined, which follows from C 1. 4
The use of a simplified subset of OCL facilities transformation verification, via
the use of semantic mappings from transformation languages into verification
formalisms and tools such as B [
The mapping from UML to B has been implemented in the UML-RSDS tools
[
The following verification properties of a UML-RSDS transformation specification τ from a source language S to a target language T can be checked using B: 1. Syntactic correctness: if a source model m of S satisfies all the assumptions Asm of τ , then the transformation will produce valid target models n from m which satisfy the language constraints ΓT of T . 2. Invariance: an invariant Inv is true throughout execution of τ .
Entity →exists(e | e.name = name and e.superclass = Set {}) This can be used to support syntactic correctness proof, i.e., that tables have unique names. Termination, confluence and semantic correctness of the implementation stat (C 1); stat (C 2) follows from the syntactic form of the constraints (that they can both be implemented by bounded loops). 5
There has been considerable work on the formalisation of OCL and UML for
semantic analysis [
We have provided arguments to justify restrictions upon OCL-style constraint specification in transformation languages, and provided examples to show the practical benefits of such restrictions.