Issue No. 03 - March (1997 vol. 23)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.585503
<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>
Abstract data type, abstraction function, abstraction mapping, abstraction relation, data abstraction, formal specification, greedy algorithm, program verification, nondeterminism, optimization problem, relation.
B. W. Weide, M. Sitaraman and W. F. Ogden, "On the Practical Need for Abstraction Relations to Verify Abstract Data Type Representations," in IEEE Transactions on Software Engineering, vol. 23, no. , pp. 157-170, 1997.