Programming in Maude is executable mathematical modeling. Your mathematical model is the code you execute. Both deterministic systems, specified equationally as so-called functional modules and concurrent ones, specified in rewriting logic as system modules, are mathematically modeled and programmed this way. But rewriting logic is also a logical framework in which many different logics can be naturally represented. And one would like not only to execute these models, but to reason about them at a high level. For this, symbolic methods that can automate much of the reasoning are crucial. Many of them are actually supported by Maude itself or by some of its tools. These methods are very general: they apply not just to Maude, but to many other logics, languages and tools. This paper presents some tapas about these Maude-based symbolic methods in an informal way to make it easy for many other people to learn about, and benefit from, them.
展开▼
