Abstract data types and software validation
Communications of the ACMPublished 1 December 1978Open access
John V. Guttag, Ellis Horowitz, David R. Musser
Citations410
SJR quartileQ1
SJR score1.15
SNIP3.34
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The major thrust of the paper is shown how the use of algebraic axiomatizations can simplify the process of proving the correctness of an implementation of an abstract data type.
Abstract
A data abstraction can be naturally specified using algebraic axioms. The virtue of these axioms is that they permit a representation-independent formal specification of a data type. An example is given which shows how to employ algebraic axioms at successive levels of implementation. The major thrust of the paper is twofold. First, it is shown how the use of algebraic axiomatizations can simplify the process of proving the correctness of an implementation of an abstract data type. Second, semi-automatic tools are described which can be used both to automate such proofs of correctness and to derive an immediate implementation from the axioms. This implementation allows for limited testing of programs at design time, before a conventional implementation is accomplished.
Keywords
Computer Science
Acta InformaticaProof of correctness of data representations
964 Citations1972C. A. R. Hoare
A powerful method of simplifying the proofs of program correctness is suggested and some new light is shed on the problem of functions with side-effects.
Communications of the ACMAbstraction mechanisms in CLU
772 Citations1977Barbara Liskov, Alan Snyder +2 more
This paper provides an introduction to the abstraction mechanisms in CLU by means of programming examples, and it is shown how CLU programs may be written to use and implement abstractions.
Studies in logic and the foundations of mathematicsA Basis for a Mathematical Theory of Computation )
699 Citations1963John McCarthy
Mathematical Theory of Computation
685 Citations1972Zohar Manna
This book is a classic text on sequential program verification; it has been widely translated from the original Hebrew and is much in demand among graduate students in the field of computer science.
Mathematical Theory of Computation
641 Citations1991John McCarthy
The goals of this project were the development of logical formalisms for reasoning about programs that use abstractions and reflection, and the application of these theoretical results to selected software problems.
Acta InformaticaThe algebraic specification of abstract data types
521 Citations1978John V. Guttag, J. J. Horning
Communications of the ACMAbstract data types and the development of data structures
462 Citations1977John V. Guttag
This paper presents and discusses the application of an algebraic technique for the specification of abstract data types and presents examples of a top-down development of a symbol table for a block structured language.
Acta InformaticaAn axiomatic definition of the programming language PASCAL
458 Citations1973C. A. R. Hoare, Niklaus Wirth
The axiomatic definition method proposed in reference [5] is extended and applied to define the meaning of the programming language PASCAL with the exception of real arithmetic and go to statements.
IEEE Transactions on Software EngineeringAn Introduction to the Construction and Verification of Alphard Programs
325 Citations1976Wm. A. Wulf, Ralph L. London +1 more
This paper introduces Alphard by developing and verifying a data structure definition and a program that uses it and 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.
FigshareInformation distribution aspects of design methodology
317 Citations2018David Lorge Parnas
The role of documentation in the design and implementation of complex systems is explored, resulting in suggestions in sharp contrast with current practice, and the thesis that such information "broadcasting is harmful, that it is helpful if most system information is hidden from most programmers, is supported.
Perceptual and Motor SkillsSIMULA 67 common base language, (Norwegian Computing Center. Publication)
172 Citations1968Ole-Johan Dahl
International Journal of Parallel ProgrammingRecursive data structures
169 Citations1975C. A. R. Hoare
A pleasing notation by which treelike data structures can be declared and processed is suggested; it gives the axioms which specify their properties, and an efficient implementation method is suggested.
International Conference on Software EngineeringThe design of data type specifications
107 Citations1976John V. Guttag, Ellis Horowitz +1 more
ACM SIGPLAN NoticesAn interactive program verification system
82 Citations1975Donald I. Good, Ralph L. London +1 more
Acta InformaticaThe verification and synthesis of data structures
57 Citations1975Jay M. Spitzen, Ben Wegbreit
How such sets of data structures may be precisely specified are discussed, an axiomatization of a programming language suitable for machine verification is presented, and how programs which realize these data structure may be proved correct are shown.
Journal of the ACMProving Properties of Complex Data Structures
39 Citations1976Ben Wegbreit, Jay M. Spitzen
ACM SIGPLAN NoticesSome extensions to algebraic specifications
34 Citations1977Jhon V. Guttag, Ellis Horowitz +1 more
The SCRATCHPAD language
21 Citations1974Richard D. Jenks
Extensions to the SCRATCHPAD language are described which enable it to serve also as a high-level programming language, both for the formal description of mathematical algorithms and their efficient implementation.
Some extensions to algebraic specifications
10 Citations1977Jhon V. Guttag, Ellis Horowitz +1 more
This paper discusses an extension to this specification technique which allows the specification of procedures which alter their parameters, and various ways of handling the Specification of error conditions.