Our previous discussion of the programming, executable specification, and formal verification uses of Maude makes clear that we can distinguish two different levels of formal specification: a system specification level, and a property specification one. In a system specification we are after an unambiguous specification of a given system and how it actually works. Ideally this specification should be both formal and executable, and should therefore provide an executable mathematical model of the system we are interested in. This is exactly what Maude modules provide.
By contrast, when specifying properties of a system we are not necessarily after an executable model of our system. Instead, we assume it, as either already given or to be developed later, and specify such properties in a typically nonexecutable manner: for example in first-order logic, higher-order logic, or some temporal logic. That is, the properties we specify have an intended model, namely the system design captured by a system specification, and we are interested in verifying by different methods that the intended model satisfies the properties stated in our property specification. In the context of Maude, such property specifications can be given in a variety of ways:
Since Maude system specifications should be both formal and executable, Maude native logics, namely, membership equational logic and its rewriting logic extension, should be computational logics, that is, logics in which computation and deduction coincides, and simple enough to allow a high-performance implementation as a declarative programming language. This is what the Maude implementation provides. Of course, as mentioned in Section 1.2 and further explained in Sections 4.6 and 5.3, Maude modules should be theories that satisfy some reasonable executability requirements, making possible not only their efficient execution, but also the already-mentioned coincidence between mathematical and operational semantics.
However, not all computational logics are equally expressive. For example, equational logics (in either first-order or higher-order versions) are very well suited to specify deterministic systems under the Church-Rosser assumption, but poorly equipped to specify concurrent and highly nondeterministic systems. The whole point of extending membership equational logic to rewriting logic is to seamlessly integrate the specification of deterministic systems, through equational specifications in functional modules, and of concurrent and nondeterministic systems, through rewriting logic specifications in system modules, within the same language. Experience has shown that this makes rewriting logic a very expressive semantic framework for system specification. Here we only mention some relevant areas:
Furthermore, other application areas can be naturally supported in appropriate extensions of rewriting logic and Maude. For example, real-time and hybrid systems can be specified as real-time rewrite theories. Such specification can be executed and analyzed in the Real-Time Maude tool [64,65]. Similarly, probabilistic systems can be specified as probabilistic rewrite theories, and can be simulated in PMaude and analyzed in the VeStA tool [49,2].
The fact that in a computational logic computation and deduction coincide, so that they are like two sides of the same coin, can be used in two ways: we can use the logic as a semantic framework to specify different computational entities as just explained; or we can use it as a logical framework to represent many other logics in it. That is, if our computational logic has good representational features, it can be used as a universal logic which can faithfully express the inference systems of many other logics.
Since the logic is computational and presumably has an efficient implementation, this is not just a purely theoretical exercise: we can use such an implementation to mechanize deduction in any logic that we can faithfully represent inside our logical framework. Experience has shown that rewriting logic has very good properties as a logical framework in precisely this sense. An important practical consequence is that it becomes quite easy to use Maude to develop a variety of formal tools for different logics. The point is that any such tool has an associated inference system, so it is just a matter of representing such an inference system as a rewrite theory and guiding the application of the inference rules with suitable strategies (see Section 11.5). In addition, since such formal tools often manipulate and transform not only formulas but also theories, Maude's reflective capabilities, which allow manipulating theories as data, become enormously useful [17,18].
Reflection and the existence of initial models (and therefore of induction principles for such models) have one further important consequence, namely, that rewriting logic has also good properties as a metalogical framework. A metalogical framework is a logical framework in which we can not only represent and simulate many other logics: we can also reason within the framework about the metalogical properties of the logics thus represented. As explained in [3], this is exactly what can be done in rewriting logic using Maude and Maude's inductive theorem prover (ITP).