Automatically checking an implementation against its formal specification

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.