Correctness proofs for abstract implementations (Q1119388)

The author claims to have a new way to present abstract data types which allows the use of standard proof techniques, such as term rewriting, to prove correctness. Unfortunately, these matters are rather complex, and it takes the author some eight or so pages to get around to saying what his new method consists of. The proof treated by this paper is the following: one is given a ``previously implemented'' data structure \((S_ 0,\Sigma_ 0,A_ 0)\), where \(S_ 0\) is a set of sorts, \(\Sigma_ 0\) is a collection of operations on these sorts, and where \(A_ 0\) is a collection of positive conditional axioms over the signature \((S_ 0,\Sigma_ 0)\). One would like to extend this data structure to a larger data structure \((S_ 1,\Sigma_ 1,A_ 1)\). The problem is to define a constructive specification of the second structure using the first, and to give usable correctness criteria. There are five steps in the author's method, and each takes a good deal of space to describe. It is claimed that this method guarantees that the composite of correct specifications is correct. I would conjecture that this is not the last word that can be said about this difficult practical problem.