[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 |