Navigation Expressions in OO Modelling

In component-based development, object-oriented modelling notations such as UML are being proposed as a way of providing richer specifications of components. Much more so than in bespoke software development, this requires a high level of precision coupled with sufficient expressive power. Expressive power is delivered by adding textual annotations, such as invariants, pre & post conditions, to diagrams. Navigation expressions, which identify collections of objects by navigating associations, are central to making such annotations precise. We give a semantics to navigation expressions as they are used in recently proposed extensions to object-oriented modelling notations in widespread use by practitioners. The semantics is given using Larch (essentially FOPL), which makes it as accessible as possible while enabling some support for reasoning. The semantics helps to clarify some subtle issues to do with navigation expressions, including the meaning of navigating across collections (sets, bags and sequences) as opposed to just single objects, and the use of filters on collections within expressions.