This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Abstract Data Type Specification in the Affirm System
January 1980 (vol. 6 no. 1)
pp. 24-32
D.R. Musser, Research and Development Center, General Electric Company
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.
Index Terms:
rewrite rules, Abstract data types, algebraic specifications, automatic theorem proving, equational theories, program verification
Citation:
D.R. Musser, "Abstract Data Type Specification in the Affirm System," IEEE Transactions on Software Engineering, vol. 6, no. 1, pp. 24-32, Jan. 1980, doi:10.1109/TSE.1980.230459
Usage of this product signifies your acceptance of the Terms of Use.