Automatic data structure selection: an example and overview <s> 376 <s> The motivation behind the work in very-high-level languages is to ease the programming task by providing the programmer with a language containing primitives or abstractions suitable to his problem area. The programmer is then able to spend his effort in the right place; he concentrates on solving his problem, and the resulting program will be more reliable as a result. Clearly, this is a worthwhile goal. ::: Unfortunately, it is very difficult for a designer to select in advance all the abstractions which the users of his language might need. If a language is to be used at all, it is likely to be used to solve problems which its designer did not envision, and for which the abstractions embedded in the language are not sufficient. ::: This paper presents an approach which allows the set of built-in abstractions to be augmented when the need for a new data abstraction is discovered. This approach to the handling of abstraction is an outgrowth of work on designing a language for structured programming. Relevant aspects of this language are described, and examples of the use and definitions of abstractions are given. <s> BIB001 </s> Automatic data structure selection: an example and overview <s> 376 <s> This paper is concerned with proving properties of programs which use data structures. The goal is to be able to prove that all instances of a class (e.g. as defined in Simula) satisfy some property. A method of proof which achieves this goal, generator induction , is studied and compared to other proof rules and methods: inductive assertions, recursion induction, computation induction, and, in some detail, structural induction. The paper concludes by using generator induction to prove a characteristic property of an implementation of hashtables. <s> BIB002 </s> Automatic data structure selection: an example and overview <s> 376 <s> The programming language Alphard is designed to provide support for both the methodologies of “well-structured” programming and the techniques of formal program verification. Language constructs allow a programmer to isolate an abstraction , specifying its behavior publicly while localizing knowledge about its implementation. The verification of such an abstraction consists of showing that its implementation behaves in accordance with its public specifications; the abstraction can then be used with confidence in constructing other programs, and the verification of that use employs only the public specifications. This paper introduces Alphard by developing and verifying a data structure definition and a program that uses it. It shows how each language construct contributes to the development of the abstraction and discusses the way the language design and the verification methodology were tailored to each other. It serves not only as an introduction to Alphard, but also as an example of the symbiosis between verification and methodology in language design. The strategy of program structuring, illustrated for Alphard, is also applicable to most of the “data abstraction” mechanisms now appearing. <s> BIB003
In the past several years computer scientists have realized that the use of several levels of abstraction in programming often gives improved results in terms of clarity, correctness, and ease of maintenance of the resulting programs. One important aspect of abstraction is the use of data types such as stacks, queues, sets, and so forth. The properties of abstract types can often be described axiomatically BIB002 BIB003 . This aids in constructing formal or informal proofs of program correctness. Several systems (CLU BIB001 , SIMULA-67  ) have gone further and shown the benefits of "hiding" the low-level implementations of the abstract types. Thus a programmer might deal with a stack only in terms of a small number of primitives upon it such as PUSHing an element, POPing an element off the stack, testing if the stack were E M P T Y , and so forth. The programmer would not have to concern himself witfi whether the underlying representation were a linked list, an array, or some hybrid. When a program is written using only primitives on an abstract type without using any knowledge of the underlying representation, the underlying representation may be changed without affecting the operation of the program except possibly for resource requirements. Given a programming system which provides the abstract type stack, a natural thing to do would be to have a number of alternative implementations of stacks and choose the implementation which is most efficient (by some criteria) for any individual program. An "intelligent" compiler would pick the "best" set of implementations for the abstract types of an individual program from a fixed library of implementations for the types. For the purpose of this paper, we define "abstract data types" to mean SIMULA-like classes which the user sees only as a number of well-defined primitives such as PUSH and POP mentioned above. The term "abstract data structure" will mean a particular instantiation of an abstract type (e.g. a particular stack). The programmer will not assume any particular representation for the abstract data structure and will manipulate it using only the given primitives. A prerequisite for selecting a good representation for an abstract data structure is a rich library of implementations for the various abstract types. Cost formulas for these primitive operations performed on the data structure must also be available. The costs will typically be functions of the size of the data structure and other properties of the data. This library of implementations and cost formulas need only be constructed once for the programming system, but the implementation specifications will be used in the compilation of each program. There are several steps in the process of selecting good representations of the data for a given program. The compiler must determine how the data structures are used within the program, their domain, their size, what operations are performed upon them, and so forth. In the prototype system described below, static flow analysis, monitoring executions of sample runs, and user interrogation provide this information. Given the above information, the system uses an implementation selection algorithm which attempts to minimize the cost (according to some fixed criteria) of executing the program. An iterative technique is used for selecting representations in the prototype system described below. In the remainder of this paper we discuss a prototype system which has been used successfully for selecting representations for sets and sequences. The selections made by this prototype system compare favorably with those made by a human programmer. The selections have differed from those that would have been made by the author in only a few cases. Those cases were typically of two type~: the system picked a more complex representation (such as AVL tree or hash table) when its utility was only marginally better than that of a simpler representation (such as bit vector or linked list); the human programmer used information not available to the automatic selection system. This prototype system could easily be extended to select representations for other reservoir-like abstract types such as queues and stacks. Later we shall give an overview of the problems which must be considered in making a practical data structure selection system.