Verifying abstract data types with SNOBOL4
A. C. Fleck · Software Practice and Experience · 1982
Abstract The presentation of an abstract data type by a series of equational axioms has become an accepted specification mechanism. Verifying the correctness of such specifications has been recognized as a problem troubling their use. A means is presented for experimenting with a directly executable version of the axioms without having to choose representations for the data structures or describe algorithms for the operations.