Integration of CafeOBJ and Maude


CafeOBJ and Maude are sister languages of the OBJ language, and two of the most advanced formal specification languages for systems verification. Although both of them have a similar syntax and semantics, different usages and applications have been developed for them. Hence, a tool combining both languages would be very useful for exploiting the specific features of each of them.

We present here how to load CafeOBJ specifications into the Full Maude. This is achieved by defining the CafeOBJ syntax and the rules for parsing these modules. Since this is the basis of all the applications built on top of Full Maude, an extra advantage of this process is that we can easily extend other tools to work with CafeOBJ specifications.

We present two examples of such an integration, the Declarative Debugger and the Constructor-based Inductive Theorem Prover (CITP). While the former works on the Maude specifications obtained after translating the CafeOBJ modules, the latter works specifically with CafeOBJ specifications, so the underlying Maude infrastructure remains hidden.

Papers

Downloads and links

Introducing CafeOBJ specifications into the Full Maude database

We present first CafeOBJ syntax by means of an example. CafeOBJ can define modules with loose semantics by using the syntax mod*. For example, we can define a module ELT requiring the existence of a sort Elt and an element of this sort, called mt, which is a constructor:

mod* ELT {
 [Elt]
 op mt : -> Elt {constr}
}
We can use this module to define a parameterized module with tight semantics, with syntax mod!. The module LIST below indicates that it receives a parameter X fulfilling the requirements stated by ELT. This modules first defines the sort List for lists:
mod! LIST(X :: ELT) {
  [List]

The constructors are defined, as shown above, with the keyword op and the constr attribute. In this case the constructors are nil for empty lists and the juxtaposition for placing an element of sort Elt in front of a list:

  op nil : -> List {constr}
  op __ : Elt.X List -> List {constr}

We can also define functions on lists. For example composition of lists is defined by distinguishing constructors on the first argument as follows:

  var E : Elt.X
  var L L' : List
  op _@_ : List List -> List
  eq [com1] : nil @ L = L .
  eq [com2] : (E L) @ L' = E (L @ L') .

Similarly, we can define the reverse function. This function uses the constant mt from module ELT as the reverse of the empty list, while the reverse for bigger lists is defined as usual by using the composition above:

  op reverse : List -> List
  eq [r1] : reverse(nil) = mt nil .
  eq [r2] : reverse(E L) = reverse(L) @ (E nil) .

Finally, we can also define non-deterministic transitions. For example, we can combine two lists by using the commutative operator mix and two transitions to indicate that the next element is the first one of any of the lists (thanks to the matching module commutativity):

  op mix : List List -> List {comm}
  trans [m1] : mix(nil, L) => L .
  trans [m2] : mix(E L, L') => E mix(L, L') .
}

We use an on-the-fly view to instantiate this module with natural numbers:

mod! NAT-LIST {
  pr(LIST(view to NAT {sort Elt -> Nat, op mt -> 0}))
}

Once the files above have been downloaded and the paths have been configured, and assuming the modules above are saved in a file called example.cafe, we can start the tool by typing:

$ ./cafe2maude example.cafe
The cafe2maude script creates a temporary file generated by the Java application parser.jar. This file contains the original CafeOBJ modules modified in order to be accepted by Full Maude (e.g. adding the parentheses enclosing modules and views, removing CafeOBJ comments, and adding the ` character to the scape characters such as { or }). Once the script is executed, the modules are introduced into the Full Maude database and we can use any Maude command on them. For example, we can use the show command to see the translated module:
Maude> (show module ELT .)
fth ELT is
  sorts Elt .
  op mt : -> Elt [ctor] .
endfth
The red command allows to simplify terms by using equations:
Maude> (red (3 2 nil) @ (2 3 nil) .)
result List : 3 2 2 3 nil
The rew command uses transitions to transform terms. Note that this command, as well as the ones described below, is not available in CafeOBJ:
Maude> (rew mix(1 3 nil, 2 4 nil) .)
result List : 1 2 3 4 nil
The search command looks for terms matching a given pattern and satisfying some conditions. For example, we can check whether the result obtained by the rew command above is the only one available:
Maude> (search mix(1 3 nil, 2 4 nil) =>! L:List
        s.t. L:List =/= 1 2 3 4 nil .)

Solution 1
L:List --> 1 3 2 4 nil

Solution 2
L:List --> 2 4 1 3 nil

Solution 3
L:List --> 1 2 4 3 nil

Solution 4
L:List --> 2 1 3 4 nil

Solution 5
L:List --> 2 1 4 3 nil

No more solutions.
where the =>! option indicates that we are looking for final states, that is, states where no more transitions can be applied. We can also use symbolic search to start with terms with variables and look for substitutions that fulfill the conditions imposed by the search. For example, we can look for the term required in the mix operator to obtain the result from the rew command:
Maude> (search [1] mix(L:List, 2 4 nil) ~>! 1 2 3 4 nil .)
Solution 1
L:List --> 1 3 nil
No more solutions.
where the ~>! option distinguishes the symbolic search from the standard one. In this case we obtain the substitution L:List --> 1 3 nil, indicating that we needed this list to obtain the result.

Besides using Maude commands, we can also work with CafeOBJ specifications. We can see the original module:

Maude> (original CafeOBJ module ELT .)
mod* ELT{
  [Elt]
  op mt : -> Elt {constr}
}
and execute proof scores. Basically, proof scores are scripts defining an inductive proof, where constants can be declared by means of operators and hypothesis by using equations. The base and the inductive steps are proved by using the red command. For example, we can prove the associativity of the _+_ function as follows:
open NAT + BOOL
 -- declaring three arbitrary numbers i, j, and k on the sort Nat:
 ops i j k : -> Nat
 -- base step:
 red (0 + j) + k == 0 + (j + k) .
 --> should be true
 -- induction hypothesis:
 eq (i + j) + k = i + (j + k) .
 -- inductive step:
 red (s(i) + j) + k == s(i) + (j + k) .
 --> should be true
close

Once we load the file with this open-close environment, Maude executes the red commands and provides the following result:

Processing open-close environment:
reduce(0 + j)+ k == 0 + j + k .
Result: true : Bool
reduce(s i + j)+ k == s i + j + k .
Result: true : Bool

Using the Maude Declarative Debugger with CafeOBJ specifications

To start this tool (note that loading this tool or the one in the next section also allows to use the commands shown in the previous section) it is enough to execute the script cdd, configure the paths, and execute it with the files we want to test and debug:

$ ./cdd example.cafe

Now, we can use all the commands described here to test and debug our CafeOBJ modules. For example, we can test the reverse function by using the so called function coverage criterium, which generates ground test cases that must use all the equations defined for reverse (r1 and r2) in all the calls (the single call to this function is located in r2). This is done by using the commands:

Maude> (function coverage .)
Function Coverage selected

Maude> (test in NAT-LIST : reverse .)
1 test cases were generater.
1 test cases have to be checked by the user:
    1. The term reverse(0 0 nil) has been reduced to 0 0 0 nil
All calls were covered.

That is, the call reverse(0 0 nil) uses both r1 and r2 for the recursive call (r2 for the first call and r1 for the second one). Note that the result of this call is unexpected, because it should also be 0 0 nil. Hence, this function is buggy and must be debugged. We can do it by typing:

Maude> (invoke debugger with user test case 1 .)
Declarative debugging of wrong answers started.

This command starts the declarative debugger. Declarative debuggers find bugs in programs by asking questions to the user, that must answer yes or no (check the webpage above for more possible answers) until the bug is found. Hence, the debugger presents the following question:

Is this reduction (associated with the equation r2) correct?
reverse(0 nil) -> 0 0 nil

Maude> (no .)

This result is erroneous for the same reasons explained above, so the user answers no and the debugging session continues with the following question:

Is this reduction (associated with the equation com2) correct?
(0 nil) @ 0 nil -> 0 0 nil

Maude> (yes .)

In this case the composition is correct, so the user answers yes. The next question is:

Is this reduction (associated with the equation r1) correct?
reverse(nil) -> 0 nil

Maude> (no .)

The answer to this question is again no. With this information the debugger is able to find the bug:

The buggy node is:
 reverse(nil) -> 0 nil
with the associated equation: r1

In fact, the equation r1 should return just nil. The questions asked during the session correspond to the nodes of a tree representing the wrong computation. This tree, which might be useful to the user to check the relations between the calls, is shown as follows:

Maude> (show tree .)
tree(r2 : reverse(0 0 nil) -> 0 0 0 nil,
      tree(r2 : reverse(0 nil) -> 0 0 nil,
            tree(r1 : reverse(nil) -> 0 nil,mt)
            tree(com2 :(0 nil) @ 0 nil -> 0 0 nil,
                  tree(com1 : nil @ 0 nil -> 0 nil,mt)))
      tree(com2 :(0 0 nil) @ 0 nil -> 0 0 0 nil,
            tree(com2 :(0 nil) @ 0 nil -> 0 0 nil,
                  tree(com1 : nil @ 0 nil -> 0 nil,mt))))

It is also possible to use a property and a correct module to test functions. For example, we can define in the module PROP-LIST the property prop stating that applying reverse twice returns the same list, while in CORRECT-PROP-LIST we state that this property must be always true:

mod! PROP-LIST {
  pr(LIST(X <= Elt))

  var L : List

  op prop : List -> Bool
  eq [p1] : prop(L) = reverse(reverse(L)) == L .
}

mod! CORRECT-PROP-LIST {
  pr(LIST(X <= Elt))

  var L : List

  op prop : List -> Bool .
  eq prop(L) = true .
}

Now we can set the correct module and generate test cases:

Maude> (correct test module CORRECT-PROP-LIST .)
CORRECT-PROP-LIST selected as correct module for testing.

Maude> (test in PROP-LIST : prop .)
10 test cases are incorrect with respect to the correct module.

Once the test cases have been generated, they can be displayed as follows:

Maude> (show 5 incorrect .)

The following test cases are incorrect with respect to the correct module:

	1. The term prop(1 1 nil) has been reduced to false

	2. The term prop(2 0 nil) has been reduced to false

	3. The term prop(4 nil) has been reduced to false

	4. The term prop(0 0 1 nil) has been reduced to false

	5. The term prop(0 1 0 nil) has been reduced to false

We can use the debugger again to debug any of this errors. For example, we can debug the first test case by using:

Maude> (invoke debugger with incorrect test case 1 .)
Declarative debugging of wrong answers started.

Is this reduction (associated with the equation r2) correct?

reverse(0 nil) -> 0 0 nil

In this case the answer to the first question is also no, for the same reasons explained above. The next question is:

Is this reduction (associated with the equation com2) correct?

(0 nil) @ 0 nil -> 0 0 nil

Maude> (yes .)

The reduction is correct, so we answer yes. The next question finishes the debugging process:

Is this reduction (associated with the equation r1) correct?

reverse(nil) -> 0 nil

Maude> (no .)

The buggy node is:
reverse(nil) -> 0 nil
with the associated equation: r1

Using the Constructor-based Inductive Theorem Prover with CafeOBJ specifications

The Constructor-based Inductive Theorem Prover (CITP), available here, allows the user to prove properties on our CafeOBJ specifications. It is started by the citp script as follows:

$ ./citp example.cafe

Since we want to prove properties on CafeOBJ specifications, we have to indicate it with a specific command, which modifies the syntax and the display options to work with CafeOBJ specifications:

Maude> (cafeOBJ language .)

CafeOBJ selected as current specification language.

Command lists:
	load *.cafe .			-- load modules into database

	(goal ModuleName |- Equations/Transitions)
	(set ind on Vars .)		-- specify the variables for induction
	(init LEMMA by V <- c .)	-- initialize a lemma by substitution.
	(auto goal GoalID .)		-- prove a subgoal
	(auto .)			-- try to prove the current goal
	(roll back .)			-- go back to the previous goal
	(apply RuleName .)		-- apply a given rule to default goal
	(apply RuleName to GoalId .)	-- apply a rule to a goal
	(cp EQ >< EQ)			-- check critical pairs
	(cp Label >< Label .)		-- check critical pairs
	(transition .)			-- add a critical pair as a transition
	(backward transition .)		-- transition in inverse direction
	(equation .)			-- add a critical pair as an equation
	(backward equation .)		-- equation in inverse direction
	(show unproved goals .)		-- show all unproved goals
	(show goal GoalID .)		-- show a goal and set it as default
	(show goal .)			-- show the current goal
	(show tactics .)		-- show all tactics
	(set tactic PROOF STRATEGY .)	-- specify customized proof strategy
	(select tactic NAT .)		-- to use customized proof strategy
	(set module off .)		-- only show added contents in module
	(set module on .)		-- display all content in modules

Note that the commands use CafeOBJ syntax, hence allowing the user to use transitions on goal and critical pairs. For example, we can prove the associativity of list composition by typing:

Maude> (goal NAT-LIST |- eq L1:List @ (L2:List @ L3:List) =
                           (L1:List @ L2:List) @ L3:List ;)
============================ GOAL 1-1 ============================
< Module NAT-LIST is concealed
...
end, eq L1:List @ (L2:List @ L3:List) = (L1:List @ L2:List) @ L3:List . >
unproved
INFO: an initial goal generated!

This goal can easily be proved by using induction on L1 and then applying the default tactic with the auto command:

Maude> (set ind on L1:List .)
INFO: Induction will be conducted on L1:List

Maude> (auto .)
INFO: Goal 1-1 was successfully proved by applying tactic: SI CA CS TC IP
INFO: PROOF COMPLETED

It is also possible to state goals involving transitions. For example, we can define the following trivial goal, which just uses the commutativity attribute:

Maude> (goal NAT-LIST |- trans mix(L:List, nil) => L ;)
============================ GOAL 1-1 ============================
< Module NAT-LIST is concealed
...
end, trans mix(L:List,nil) => L:List . >
unproved
INFO: an initial goal generated!

Note that CafeOBJ syntax is used for both the goal and the displayed information. This simple goal can be discarded by just using auto:

Maude> (auto .)
INFO: Goal 1-1 was successfully proved
by applying tactic: SI CA CS TC IP
INFO: PROOF COMPLETED

Questions and comments are welcome ariesco[AT]fdi.ucm.es.