A Tool Support for Reusing ELAN Rule-Based Components

The adaptation of software components developed for a specific application in order to generate reusable components often includes some kind of generalization. This generalization may be carried out, for instance, by the renaming of some identifiers or by its parameterization. In our work, we are specially interested in the generalization by parameterization of algebraic specification components. Generalization and some other transformations on algebraic specifications are being integrated in the FERUS tool. This tool was initially developed for the Common Algebraic Specification Language, called CASL, and we show in the paper its adaptation to the new version of the rule-based programming language ELAN.     

Polite Combination of Algebraic Datatypes

Journal of Automated Reasoning - Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its...     

Combination of convex theories: Modularity,deduction completeness,and explanation

Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple “sat/unsat” answer. In this paper, we develop a framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the framework to specify and prove the correctness of classic combination schemas by Nelson–Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them for large classes of theories, then we provide a schema to modularly combine them. Third, we consider the problem of modularly constructing explanations for combinations by re-using available proof-producing procedures for the component theories.     

A Pattern-Matching Compiler

Implementation of a rule-based transformation engine consists of several tasks with various abstraction levels. We present a new tool called mtom for the efficient implementation of rule-based transformations. This engine should help to bridge the gap between rewriting implementations and practical applications. It aims at implementing well-identified parts of complex applications where the use of rewriting is natural or crucial. These parts are specified using rewrite rules and integrated with the rest of the application, which is kept in a classical imperative language such as C, C++ or Java. Our tool, which can be viewed as a Yacc-like pre-processor, does not depend on a given term representation, rather it accepts implementation of terms (or term like data-types) of yet existing applications and it permits to define and execute rewrite rules upon those types. From our experiences, this system is well-suited for industrial use as well as for implementations of rule-based languages. The paper introduces several features supported by mtom.     

Timed Specification For Web Services Compatibility Analysis

Web services are becoming one of the main technologies for designing and building complex inter-enterprise business applications. Usually, a business application cannot be fulfilled by one Web service but by coordinating a set of them. In particular, to perform a coordination, one of the important investigations is the compatibility analysis. Two Web services are said compatible if they can interact correctly. In the literature, the proposed frameworks for the services compatibility checking rely on the supported sequences of messages. The interaction of services depends also on other properties, such that the exchanged data flow. Thus, considering only supported sequences of messages seems to be insufficient. Other properties on which the services interaction can rely on, are the temporal constraints. In this paper, we focus our interest on the compatibility analysis of Web services regarding their (1) supported sequences of messages, (2) the exchanged data flow, (3) constraints related to the exchanged data flow and (4) the temporal requirements. Based on these properties, we study three compatibility classes: (i) absolute compatibility, (ii) likely compatibility and (iii) absolute incompatibility.     

Combining Decision Algorithms for Matching in the Union of Disjoint Equational Theories

This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theoriesE₁∪E₂provided that matching algorithms are known in both theoriesE₁andE₂. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms (with linear constant restriction) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way.     

Automatic decidability and combinability

Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory T axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of T decidable by paramodulation? Can a procedure based on paramodulation for T be efficiently combined with other specialized procedures by using the Nelson-Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union?The procedure capable of answering all questions above is based on Schematic Saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory T. Clause schemas derived by Schematic Saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived.