We propose checking the execution of an abstract data type's imperative imp
lementation against its algebraic specification. An explicit mapping from i
mplementation states to abstract values is added to the imperative code. Th
e form of specification allows mechanical checking of desirable properties
such as consistency and completeness, particularly when operations are adde
d incrementally to the data type. During unit testing, the specification se
rves as a test oracle. Any variance between computed and specified values i
s automatically detected. When the module is made part of some application,
the checking can be removed, or may remain in place for further validating
the implementation. The specification, executed by rewriting, can be thoug
ht of as itself an implementation with maximum design diversity, and the va
lidation as a form of multiversion-programming comparison.