×
Wand, Mitchell

Specifications, models, and implementations of data abstractions. (English) Zbl 0478.68021

Theor. Comput. Sci. 20, 3-32 (1982).
Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page
scan of Zbl 0478.68021

Cited in 1 Review
Cited in 5 Documents

MSC:

68P05 Data structures

Keywords:

verification of modules; DLP; specification language; first order dynamic logic; abstract data types
Cite Review PDF
Full Text: DOI

References:

[1] Church, A., Introduction to Mathematical Logic, Vol. I (1956), Princeton University Press: Princeton University Press Princeton, NJ · Zbl 0073.24301
[2] Correll, C. H., Proving programs correct through refinement, Acta Informat., 9, 121-132 (1978) · Zbl 0367.68010
[3] Dahl, O. J.; Hoare, C. A.R., Hierarchical program structures, (Dahl, O. J.; Dijkstra, E. W.; Hoare, C. A.R., Structured Programming (1972), Academic Press: Academic Press London), 175-220
[4] Dijkstra, E. W., Notes on structured programming, (Dahl, O. J.; Dijkstra, E. W.; Hoare, C. A.R., Structured Programming (1972), Academic Press: Academic Press London) · Zbl 0418.68032
[5] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[6] H.D. Ehrich, Extensions and implementations of abstract data type specifications, Universitat Dortmund, Report 55⧸78.; H.D. Ehrich, Extensions and implementations of abstract data type specifications, Universitat Dortmund, Report 55⧸78. · Zbl 0382.68028
[7] Ehrig, H.; Kreowski, H. J.; Padawitz, P., Algebraic implementation of abstract data types: concept, syntax, semantics and correctness, Proc. 7th Colloquium on Automata, Languages, and Programming, 142-146 (1980) · Zbl 0457.68019
[8] Elgot, C. C.; Snyder, L., On the many facets of lists, Theoret. Comput. Sci., 5, 275-306 (1977) · Zbl 0384.68013
[9] Enderton, H. B., A Mathematical Introduction to Logic (1972), Academic Press: Academic Press New York · Zbl 0298.02002
[10] Gaudel, M. C., Specifications incomplètes mais suffisantes de la representation des types abstraits, IRIA Research Report No. 320 (1978)
[11] Goguen, J.; Nourani, F., Some algebraic techniques for proving correctness of data type implementations, extended abstract (1978)
[12] Goguen, J. A.; Thatcher, J. W.; Wagner, E. G., An initial algebra approach to the specification, correctness, and implementation of abstract data types, (Yeh, R., Current Trends in Programming Methodology, IV: Data Structuring (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 80-149
[13] Guttag, J. V.; Horowitz, E.; Musser, D. R., Abstract data types and software validation, Comm. ACM, 21, 1048-1064 (1978) · Zbl 0387.68012
[14] Harel, D.; Meyer, A. R.; Pratt, V. R., Computability and completeness in logics of programs, Proc. 9th Annual ACM Symposium on Theory of Computing, 261-268 (1977)
[15] Harel, D.; Pratt, V. R., Nondeterminism in logics of programs, Conference Records 5th ACM Conference on Principles of Programming Languages, 203-213 (1978)
[16] Hoare, C. A.R., Proving correctness of data representations, Acta Informat., 1, 271-281 (1972) · Zbl 0244.68009
[17] Hofstadter, D. R., Gödel, Escher, Bach: An Eternal Golden Braid (1979), Basic Books: Basic Books New York · Zbl 1014.03005
[18] Kamin, S., Final data type specifications: a new data type specification method, Conference records 7th ACM Symposium on Principles of Programming Languages, 131-138 (1980)
[19] Knuth, D. E.; Pardo, L. T., The early development of programming languages, (Belzer, J.; Holtzman, A. G.; Kent, A., Encyclopedia of Computer Science and Technology, Vol. 6 (1977), Dekker: Dekker New York), 419-493
[20] Lehmann, D. J.; Smyth, M. B., Data types, (Theory of Computation Report No. 19 (1977), University of Warwick)
[21] Liskov, B.; Snyder, A.; Atkinson, R.; Schaffert, C., Abstraction mechanisms in CLU, Comm. ACM, 20, 564-576 (1977) · Zbl 0362.68018
[22] Liskov, B.; Zilles, S., Specification techniques for data abstractions, IEEE Trans. Software Engrg., 1, 7-19 (1975)
[23] MacLane, S., Categories for the Working Mathematician (1971), Springer: Springer New York · Zbl 0232.18001
[24] Majster, M. E., Limits of the algebraic specification of data types, SIGPLAN Notices, 12, 10, 37-42 (1977) · Zbl 0348.68026
[25] Musser, D. R., A proof rule for functions, (Technical Report ISI⧸RR-77-62 (1977), University of Southern California Information Sciences Institute: University of Southern California Information Sciences Institute Marina del Rey, CA)
[26] Nakajima, R.; Honda, M.; Nakahara, H., Hierarchical program specification and verification—a many-sorted logical approach, Acta Informat., 14, 135-155 (1980) · Zbl 0432.68011
[27] Parikh, R., A decidability result for a second order process logic, Proc. 19th Annual IEEE Symposium on Foundations of Computer Science, 177-183 (1978)
[28] Parnas, D. L., A technique for module specification with examples, Comm. ACM, 15, 330-336 (1972)
[29] Pratt, V. R., Semantical considerations on Floyd-Hoare logic, Proc. 17th IEEE Symposium on Foundations of Computer Science, 109-121 (1976)
[30] Pratt, V. R., Six lectures on dynamic logic (1978), Massachusetts Institute of technology, Laboratory for Computer Science MIT⧸LCS⧸TM-117 · Zbl 1283.03066
[31] Robinson, L.; Levitt, K. N., Proof techniques for hierarchically structured programs, Comm. ACM, 20, 271-283 (1977) · Zbl 0358.68030
[32] Salwicki, A., On algorithmic theory of stacks, (Winkowski, J., Mathematical Foundations of Computer Science 1978. Mathematical Foundations of Computer Science 1978, Lecture Notes in Computer Science, 64 (1978), Springer: Springer Berlin), 452-461 · Zbl 0387.68027
[33] Shoenfield, J. R., Mathematical Logic (1967), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0155.01102
[34] Spitzen, J. M.; Levitt, K. N.; Robinson, R., An example of hierarchical design and proof, Comm. ACM, 21, 1064-1075 (1978) · Zbl 0387.68010
[35] Stoy, J. E., Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (1977), MIT Press: MIT Press Cambridge, MA · Zbl 0503.68059
[36] Tarski, A., Introduction to Logic and to the Methodology of Deductive Sciences (1946), Oxford University Press: Oxford University Press New York
[37] Wand, M., Final algebra semantics and data type extensions, J. Comput. System Sci., 19, 27-44 (1979) · Zbl 0418.68020
[38] Wulf, W. A.; London, R. L.; Shaw, M., An introduction to the construction and verification of Alphard programs, IEEE Trans. Software Engrg., 2, 253-265 (1976) · Zbl 0351.68004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.