The starting point of this paper is a system described in form of a UML class
diagram where system states are characterized by OCL invariants and system
transitions are defined by OCL pre- and postconditions. The aim of our approach
is to assist the developer in learning about the consequences of the described
system states and transitions and about the formal implications of the
properties that are explicitly given.