Null considered harmful (for transformation verication)

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.