The universal adoption of UML for object-oriented modeling notwithstanding, a major impediment for UML 1.4 is the lack of seamless integration between the different models and the inadequate support for diagram interchange. In this paper we propose a process generating formal object-oriented specifications in OCL and class diagrams from the use case model of a system through a clearly defined sequence of model transformations. The algebraic invariant of values exchanged in a use case guides the derivation of state machine descriptions for the actors and counter-actors, collectively called agents of the use case. The use case specification is obtained as the composition of the agents? state machines. We present an algorithm for converting a narrative use case specification to a set of OCL expressions and/or class diagrams. The proposed approach fills the gap between the outside behavioral system description as offered by use cases and the "first cut" at software architecture, the analysis level class model.