Programming, specification, and verification

The observations in the previous section about the agreement between mathematical and operational semantics in Maude programs are of enormous importance for reasoning about them and verifying their correctness. The key point is that there are three different uses of Maude modules:

1. As programs, to solve some application. In principle we could have programmed such an application in some other programming language, but we may have chosen Maude because its features make the programming task easier and simpler.

2. As formal executable specifications, that provide a rigorous mathematical model of an algorithm, a system, a language, or a formalism. Because of the agreement between operational and mathematical semantics, this mathematical model is at the same time executable. Therefore, we can use it as a precise prototype of our system to simulate its behavior. The system itself could be implemented in a conventional language, or perhaps in Maude itself (as in (1) above) as a more detailed Maude program, or maybe our specification is already detailed and efficient enough to be directly used as its own implementation.

3. As models that can be formally analyzed and verified with respect to different properties expressing various formal requirements. For example, we may want to prove that our Maude module terminates; or that its equations have the Church-Rosser property; or that a given function, equationally defined in the module, satisfies some properties expressed as first-order formulas. Similarly, given a system module we may want to model check some properties about it, such as the satisfaction of some invariants or, more generally, of some temporal logic formulas.

Note that the distinction between uses (1) and (2) is, for the most part, in the eyes of the beholder. In fact, there is a seamless integration of specifications and code. The same Maude module can simultaneously be viewed as an executable formal specification and as a program. Furthermore, certain kinds of formal requirements needed for verification in (3) can be expressed at the Maude level, either in Maude theories (see Section 6.3.1), or by including some nonexecutable statements in a Maude module giving them the nonexec attribute (see Section 4.5.3). This can be very useful in several ways. For example, we may include lemmas that we have proved about a module, either in theories or as nonexecutable statements in the module itself. Similarly, we may begin with some nonexecutable specifications in a Maude theory, and then refine them using views (see Section 6.3.2) into the desired Maude module satisfying them.

There is, however, no need for all the properties that we wish to formally verify in (3) to be in the logic of Maude, that is, to be statements in membership equational logic or in rewriting logic. More generally, properties can be expressed, for example, as arbitrary first-order logic formulas, or as temporal logic formulas. An interesting issue is then to explain precisely what it means for a Maude module, defined in membership equational logic or in rewriting logic, to satisfy a formula in one of those logics. Here is where the Maude initial model semantics explained in Section 1.2 becomes crucial. Such a semantics means that what a Maude module denotes is a specific mathematical model, namely, the initial one. Satisfaction of any property, expressed as some kind of formula, means satisfaction of that formula in the initial model. This is an important observation, even when the formula in question is expressed in Maude's native logic. Let us explain this idea in more detail.

Consider, for example, that we have defined natural number addition in a Maude functional module with Peano notation, so that zero is represented as the constant 0, and there is a successor function s_ so that, for example, 2 is represented as s s 0. Natural number addition can then be defined by the equations

  op _+_ : Nat Nat -> Nat .
  vars N M K : Nat .
  eq N + 0 = N .
  eq N + (s M) = s (N + M) .

The initial model of these equations is precisely the algebra of the natural numbers with zero, successor, and the usual addition function. For example, using the canonical term algebra representation (see Section 1.2), when we add s s 0 and s s 0 in this algebra we obtain the result s s s s 0.

Consider now two relevant properties of natural number addition, namely, associativity and commutativity. These properties are precisely described by the respective equations

  eq N + M = M + N [nonexec] .
  eq N + (M + K) = (N + M) + K [nonexec] .

where we have used the nonexec attribute to emphasize that these equations are not part of our natural number addition module, and are not meant to be executed (in fact, if executed the first equation would loop). They may, for example, be stated in a separate Maude theory as properties we wish to verify.

The first thing to observe is that the above associativity and commutativity equations are not provable by equational deduction, that is, they do not follow by replacing equals by equals from the two equations defining the addition function. They are in fact inductive properties of the addition function. Therefore, in order to prove them, using for example Maude's inductive theorem prover (ITP), we need to use a stronger proof method, namely, Peano induction. But for any equational specification, being an inductive property and being a property satisfied by its initial model are one and the same thing [61]. Therefore, what we mean when we say that our natural number addition module satisfies the associativity and commutativity equations is precisely that its initial model does.

Of course, associativity and commutativity are properties expressible in Maude's native logic (in fact, just in its equational sublogic). But the case of arbitrary first-order formulas is entirely similar. Consider, for example, the property that any even number is the sum of two odd numbers, which can be expressed as the first-order formula

$$\forall n: \mathit{Nat} \; (\mathit{even}(n) \;\; \Longrighta... ...; (\mathit{odd}(x) \wedge \mathit{odd}(y) \wedge n = x + y)) .$$

Let us assume, for argument's sake, that we had also defined the odd and even predicates in our Maude natural number module. What does it mean for our module to satisfy the above formula? Just as before, it exactly means that the initial model denoted by our Maude specification satisfies the formula. The point is that membership equational logic is a sublogic of many-kinded first-order logic with equality (MKFOL$^{=}$) that we can represent with a sublogic inclusion

$$\mbox{MEqLogic} \hookrightarrow \mbox{MKFOL$^{=}$}.$$

Therefore, our initial model is also a first-order logic model, and it is perfectly clear what it means for it to satisfy a first-order formula.

In a similar way, if we have a Maude system module and choose an initial state for it, we may be interested in verifying that it satisfies a given temporal logic formula. Defining satisfaction in this case is not as direct as for first-order formulas, because we do not have a sublogic inclusion from rewriting logic into temporal logic. However, the meaning of satisfaction in this case is also fairly straightforward. The point is that to such a system module, that is, to a rewrite theory in which we have defined some atomic state predicates equationally, we can naturally associate a Kripke structure (see Section 10.2). Since Kripke structures are the standard models of temporal logic, satisfaction of the given temporal logic formula exactly means that the Kripke structure associated to the module satisfies the formula. In fact, such a Kripke structure and the initial model of the rewrite theory are intimately related, so that the initial model can be used to define the corresponding Kripke structure. As explained in Chapters 9 and 10, if our system module is such that the set of states reachable from the initial state is finite, we can use Maude's search command and Maude's model checker for linear temporal logic (LTL) as decision procedures to verify, respectively, the satisfaction of invariants and of LTL properties.

Besides being able to use Maude's inductive theorem prover (ITP) to verify inductive properties of functional modules, and the above-mentioned built-in support for verifying invariants and LTL formulas through the search command and Maude's LTL model checker, we can use the following Maude tools to formally verify other properties:

• the Maude Termination Tool (MTT) [29] can be used to prove termination of functional modules (see Section 9.4);
• the Maude Church-Rosser Checker (CRC) [17,30] can be used to check the Church-Rosser property of unconditional functional modules (see Section 9.4);
• the Maude Coherence Checker (ChC) can be used to check the coherence (or ground coherence) of unconditional system modules (see Section 9.4); and
• the Maude Sufficient Completeness Checker (SCC) [46] can be used to check that defined functions have been fully defined in terms of constructors (see Sections 4.4.3 and 9.4).

Furthermore, if we are dealing with rewriting logic specifications of real-time and hybrid systems, we can use the Real-Time Maude tool to both simulate such specifications and to perform search and model-checking analysis of their LTL properties [64,65].

In summary, therefore, Maude supports three seamlessly integrated tasks: programming, executable formal specification, and formal analysis and verification. For analysis and verification purposes, the Maude interpreter itself is the first and most obvious tool. It is in fact a high-performance logical engine that can be used to prove certain kinds of logical facts about our theories. For example, we can use the Maude interpreter as a decision procedure for equational deduction if the desired theory has good properties. Similarly, as already mentioned, we can use it also to verify invariants and LTL properties of finite-state system modules. More generally, we can use other tools in Maude's formal environment, such as the ITP, MTT, CRC, ChC, and SCC tools (or Real-Time Maude for real-time systems) to formally verify a variety of other properties.