Abstract Data Type Specification in the Affirm System

DOI10.1109/TSE.1980.230459zbMath0431.68022WikidataQ111898002 ScholiaQ111898002MaRDI QIDQ3868738

David R. Musser

Publication date: 1980

Published in: IEEE Transactions on Software Engineering (Search for Journal in Brave)

zbMATH Keywords

theorem provingprogram verificationequational theoriesrewrite rulesabstract data type specification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items

On sufficient-completeness and related properties of term rewriting systems, History and basic features of the critical-pair/completion procedure, Sufficient-completeness, ground-reducibility and their complexity, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Hoare's logic and Peano's arithmetic, Unnamed Item, Narrowing based procedures for equational disunification, Unification modulo lists with reverse relation with certain word equations, A constructive method for abstract algebraic software specification, Partial completion of equational theories