Object Constraint Language (OCL) is a formal language used to describe expressions like constraints or queries over objects in a UML model. The constraints are used to give an exact description of the information contained in the models and the queries are used to analyze these models and to validate them. The evaluation of the OCL expressions does not have side effects. In spite of the fact OCL has defined more than ten years ago, it is not yet widely adopted in industry and one reason for that is the lack of proper and integrated tool support for OCL. Another reason is that although designed to be a formal language, experience has shown that the language definition is not precise enough. Even the last OMG standard includes underspecified things and some inconsistencies. In this paper we present an executable formal semantics for a representative fragment of OCL described in K, a semantic framework suitable for defining programming languages, type systems, formal analysis tools and calculi. K has been already successfully used for giving formal definitions to several programming languages and developing analysis tools for these languages. Therefore having a formal definition for OCL in this framework has several advantages including executability (the K semantics of OCL can be used to evaluate OCL expressions for different models), an easy integration with model languages and object-oriented languages defined in K.