• DocumentCode
    750946
  • Title

    Abstract Data Type Specification in the Affirm System

  • Author

    Musser, David R.

  • Author_Institution
    Research and Development Center, General Electric Company
  • Issue
    1
  • fYear
    1980
  • Firstpage
    24
  • Lastpage
    32
  • Abstract
    This paper describes the data type definition facilities of the AFFIRM system for program specification and verification. Following an overview of the system, we review the rewrite rule concepts that form the theoretical basis for its data type facilities. The main emphasis is on methods of ensuring convergence (finite and unique termination) of sets of rewrite rules and on the relation of this property to the equational and inductive proof theories of data types.
  • Keywords
    Abstract data types; algebraic specifications; automatic theorem proving; equational theories; program verification; rewrite rules; Contracts; Convergence; Equations; Formal specifications; Helium; Interactive systems; Intersymbol interference; Message systems; Specification languages; System testing; Abstract data types; algebraic specifications; automatic theorem proving; equational theories; program verification; rewrite rules;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/TSE.1980.230459
  • Filename
    1702691
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=750946