The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - March (1997 vol.23)
pp: 157-170
ABSTRACT
<p><b>Abstract</b>—The typical correspondence between a concrete representation and an abstract conceptual value of an abstract data type (ADT) variable (object) is a many-to-one function. For example, many different pointer aggregates give rise to exactly the same binary tree. The theoretical possibility that this correspondence generally should be relational has long been recognized. By using a nontrivial ADT for handling an optimization problem, we show why the need for generalizing from functions to relations arises naturally in practice. Making this generalization is among the steps essential for enhancing the practical applicability of formal reasoning methods to industrial-strength software systems.</p>
INDEX TERMS
Abstract data type, abstraction function, abstraction mapping, abstraction relation, data abstraction, formal specification, greedy algorithm, program verification, nondeterminism, optimization problem, relation.
CITATION
Murali Sitaraman, Bruce W. Weide, William F. Ogden, "On the Practical Need for Abstraction Relations to Verify Abstract Data Type Representations", IEEE Transactions on Software Engineering, vol.23, no. 3, pp. 157-170, March 1997, doi:10.1109/32.585503
329 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool