@inproceedings{AntoyForcheriGannonMolfino96DISCO
    ,author={S. Antoy and P. Forcheri and J. Gannon and M. T. Molfino}
    ,title={Equational Specifications: Design, Implementation, and Reasoning}
    ,year={1996}
    ,pages={126-144}
    ,publisher={Springer, Texts and monographs in symbolic computation}
    ,booktitle={Advances in the Design of Symbolic Computation Systems}
    ,abstract={
        Sets of equations can be used to specify, implement, and
        reason about software. We discuss how to automate these tasks for
        constructor-based, convergent rewrite systems. Using incremental
        design strategies, we obtain completely defined, consistent, and
        sufficiently complete specifications. Direct implementations of
        specifications as term rewriting systems serve as software
        prototypes of systems. We use prototypes to determine that
        specifications are consistent with our intuitive expectations
        during design and with more efficient implementations during
        testing. We describe an automated tool for reasoning about both
        the properties a specification and the correctness of its
        implementation. Our approach is applicable to a relatively small
        class of specifications, but within this class it appears to be
        effective for designing high quality specifications and for
        effectively using these specifications for a variety of other
        tasks arising during the software lifecycle.}
}