Analysing UML use cases as contracts

The Unified Modeling Language (UML) consists in a set of diagrams that describe a system under development. A use case diagram specifies the required functionality of the system, showing the collaboration among a set of actors that are to perform certain tasks. We complement the use case diagrams by providing formal documents (like specifications or programs), called contracts that regulate the behaviour of the actors involved. The contract is written in a language with a precise semantics and logic for reasoning - the refinement calculus - and thus it can be analysed. To express contracts we need to specify the problem domain of the system; we describe classes and UML class diagrams using also the refinement calculus. Thereby, we integrate the functional view of a system, described by the use case diagram with the object-oriented view for the same system, described by the class diagram.