Abstract
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 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.