From FSL
Jump to: navigation, search
a tool for studying totality of partial specifications
by Traian Florin Șerbănuță



This tool is a realisation of the algorithm described in [1,2] for testing wether an executable specification in partial memebership equational logic can be regarded "as is" to be a specification in (non-partial) membership equational logic. More precisely, the algorithm tests wether the given specification is equivalent in the total world with its envelope.

For more information get the report in the Download section.


  • start Maude;
  • load duplex.maude
  • load file containing the partial specification
  • commands:
  • red in DUPLEX : isDuplex?(Name,Bool) .
where Name is the quoted name of the module to be tested and Bool is the same switch as upModule accepts (tells wether to build a module taking into account all the import commands or not). This command will return true if the given theory is a duplex. If it fails to prove automatically the duplex property then it will print the goals which it could not solve.
  • red in DUPLEX : envelope(Name, Bool) .
with the same meaning for the arguments as above returns the envelope of Name.



1. Jose Meseguer, Grigore Rosu, A Total Approach to Partial Algebraic Specification.

International Colloquium on Automata, Languages, and Programming, (ICALP'02)
Lecture Notes in Computer Science, Volume 2380, pages 572-584, 2002

2. Jose Meseguer. Membership Algebra as a Logical Framework for Equational Specification.

In 12th International Workshop on Recent Trends in Algebraic Development Techniques (WADT'97),
Lecture Notes in Computer Science, Vol. 1376, pp. 18-61. 1998

3. Horst Reichel. Initial Computability Algebraic Specifications and Partial Algebras.

Oxford Science Publications, 1987
Personal tools