This paper presents a formal definition of Alan. Alan is a programming language that aims to integrate both the agent-oriented and the object-oriented programming. The end is to take advantages from both the paradigms. We want to explore how we can reason in terms of encapsulation, inheritance, polymorphism, and so on while we program in terms of the the beliefs, the desires, and the plans of an agent. We define the formal specification of Alan in the rewriting logic language Maude. In this respect, this paper represents the first step towards a complete formal definition of the operational semantics of Alan. This opens us the possibilty of using the wide-spectrum of formal modeling and reasoning supported by Maude: analyzing Alan programs by means of model checking, proving properties of particular Alan programs, and proving general properties of the Alan language.