# DUPLEX

From FSL

- a tool for studying totality of partial specifications
- by Traian Florin Șerbănuță

## Contents |

## Introduction

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.

## Usage

- 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*.

- red in DUPLEX : isDuplex?(

## Download

- DUPLEX report pdf or html
- Source code
- Some partial specifications (most of them inspired from [3])

## References

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