Access Restriction

Author Horowitz, Ellis ♦ Guttag, John V. ♦ Musser, David R.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Data type ♦ Correctness proof ♦ Specification ♦ Data structure ♦ 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.
Description Affiliation: Univ. of Southern California, Los Angeles (Guttag, John V.; Horowitz, Ellis; Musser, David R.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 21
Issue Number 12
Page Count 17
Starting Page 1048
Ending Page 1064

Open content in new tab

   Open content in new tab
Source: ACM Digital Library