Mobile Maude is a Mobile Agent language extending the rewriting logic language Maude and supporting mobile computation.  Mobile Maude uses reflection to obtain a simple and general declarative mobile language design and makes possible strong assurances of mobile agent behavior. The formal semantics of Mobile Maude is given by a rewrite theory in rewriting logic. Since this specification is executable, it can be used as a prototype of the language, in which mobile agent systems can be simulated. The two key notions are processes and mobile objects. Processes are located computational environments where mobile objects can reside. Mobile objects have their own code, can move between different processes in different locations, and can communicate asynchronously with each other by means of messages. Mobile Maude's key characteristics include: (1) reflection as a way of endowing mobile objects with higher-order capabilities; (2) object-orientation and asynchronous message passing; and (3) a simple semantics without loss in the expressive power of application code.   Mobile Maude has been specified and prototyped in Maude.
Maude Specifications and Samples

[Maude Home Page]