Correctness proofs for abstract implementations (Q1119388)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Correctness proofs for abstract implementations |
scientific article |
Statements
Correctness proofs for abstract implementations (English)
0 references
1989
0 references
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.
0 references
correctness proofs
0 references
abstract data types
0 references
0 references