Formal specification of agent-object oriented programs

This paper presents a methodology for the formal specification of agent-object oriented programs. Agent-object oriented programming is a programming paradigm that integrates both agent-oriented programming and object- oriented programming (e.g, see Jack, Jadex). Even if there are several formal specification frameworks and methodologies both for agent-oriented programs and for object- oriented programs, nothing exists for agent-object programming. In this paper, the rewriting logic language Maude has been used as a formal framework. This opens to us the possibility of using the wide-spectrum of formal modeling and reasoning supported by Maude: analyzing agent-object programs by means of execution, search, model checking, or theorem proving to verify properties of a given program such as goal satisfaction and plan termination.