Abstract Data Type Specification in the Affirm System
- 1 January 1980
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. SE-6 (1) , 24-32
- https://doi.org/10.1109/tse.1980.230459
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
This publication has 22 references indexed in Scilit:
- On proving inductive properties of abstract data typesPublished by Association for Computing Machinery (ACM) ,1980
- A simplifier based on efficient decision algorithmsPublished by Association for Computing Machinery (ACM) ,1978
- Proof rules for the programming language EuclidActa Informatica, 1978
- Abstract data types and the development of data structuresCommunications of the ACM, 1977
- Subgoal inductionCommunications of the ACM, 1977
- Abstraction mechanisms in CLUPublished by Association for Computing Machinery (ACM) ,1977
- An interactive program verification systemIEEE Transactions on Software Engineering, 1975
- The verification and synthesis of data structuresActa Informatica, 1975
- Tree-Manipulating Systems and Church-Rosser TheoremsJournal of the ACM, 1973
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965