The method of algebraic specification by abstract data types
is demonstrated by several examples, including general storage and
access systems and open hash tables. Then, after sketching the algebraic
background, correct realizations of data types are considered. Several
correctness proofs are outlined. Finally, problems corresponding to an
appropriate notion of realization are discussed.