Abstract data types and software validation
From MaRDI portal
Publication:4168047
DOI10.1145/359657.359666zbMath0387.68012OpenAlexW2015874281WikidataQ111901043 ScholiaQ111901043MaRDI QIDQ4168047
Ellis Horowitz, David R. Musser, J. V. Guttag
Publication date: 1978
Published in: Communications of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/359657.359666
Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)
Related Items
Structured theory presentations and logic representations, On sufficient completeness of conditional specifications, Design strategies for rewrite rules, Data abstraction in Prolog/KR, Implicit induction in conditional theories, An overview of LP, the Larch Prover, Crypt-equivalent algebraic specifications, Proving entailment between conceptual state specifications, Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study, Equational specification of partial higher-order algebras, Program testing: Specification languages and automatic test generation, Unnamed Item, Final algebra semantics and data type extensions, Hierarchical program specification and verification - a many-sorted logical approach, On the algebra of order, On new roles for categorical algebra, Quantifiability: a concurrent correctness condition modeled in vector space, Straight-line program length as a parameter for complexity analysis, About the implementability and the power of equationally defined data abstractions, Parallel tree pattern matching, Hierarchical development of programming languages, Specifications, models, and implementations of data abstractions, Algebraic implementation of abstract data types, Graph grammars and operational semantics, Algebraic implementation of abstract data types: a survey of concepts and new compositionality results, A Noetherian and confluent rewrite system for idempotent semigroups, Abstract data types and algebraic semantics of programming languages, Specification and proof in membership equational logic, Using induction and rewriting to verify and complete parameterized specifications, Transformations and confluence for rewrite systems, From Grammars and Automata to Algebras and Coalgebras, Unnamed Item, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, Proving programs correct through refinement, Unification modulo lists with reverse relation with certain word equations, Swinging types=functions+relations+transition systems, Approximation properties of abstract data types, Relative complexity of algebras, Methodical specification of abstract data types via rewriting systems, A set-theoretic semantics for Clear, Implementation of data types by algebraic methods, Partial completion of equational theories, Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories, On the data type extension problem for algebraic specifications, Rewrite systems on a lattice of types, Termination orderings for associative-commutative rewriting systems
Uses Software
