{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,19]],"date-time":"2022-12-19T03:25:11Z","timestamp":1671420311573},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1984,10,1]],"date-time":"1984-10-01T00:00:00Z","timestamp":465436800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1984,10]]},"DOI":"10.1007\/bf00264252","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T07:04:43Z","timestamp":1096441483000},"page":"293-320","source":"Crossref","is-referenced-by-count":6,"title":["The axiomatic semantics of programs based on Hoare's logic"],"prefix":"10.1007","volume":"21","author":[{"given":"J. A.","family":"Bergstra","sequence":"first","affiliation":[]},{"given":"J. V.","family":"Tucker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K.R. Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare's logic. A Survey: Part 1. ACM Trans. Progr. Lang. Syst. 3, 431?483 (1981)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"CR2","first-page":"115","volume":"7","author":"H. Andreka","year":"1978","unstructured":"Andreka, H., Nemeti, I.: Completeness of Floyd Logic. Bull. Sect. Logic Wroclaw 7, 115?121 (1978)","journal-title":"Bull. Sect. Logic Wroclaw"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0304-3975(82)90004-4","volume":"17","author":"H. Andreka","year":"1982","unstructured":"Andreka, H., Nemeti, I., Sain, I.: A complete logic for reasoning about programs via non-standard model theory. Theor. Comput. Sci. 17, 193?212 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"CR4","series-title":"Lecture Notes in Computer Science 118","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-10856-4_82","volume-title":"Mathematical Foundations of Computer Science 1981","author":"H. Andreka","year":"1981","unstructured":"Andreka, H., Nemeti, I., Sain, I.: A characterization of Floyd-provable programs. In: Mathematical Foundations of Computer Science 1981, Lecture Notes in Computer Science 118. Berlin, Heidelberg, New York: Springer, pp. 162?171, 1981"},{"key":"CR5","volume-title":"Mathematical theory of program correctness","author":"J.W. Bakker de","year":"1980","unstructured":"de Bakker, J.W.: Mathematical theory of program correctness. London: Prentice-Hall 1980"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(82)90001-9","volume":"17","author":"J.A. Bergstra","year":"1982","unstructured":"Bergstra, J.A., Tiuryn, J., Tucker, J.V.: Floyd's Principle, correctness theories and program equivalence. Theor. Comput. Sci. 17, 113?149 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0304-3975(82)90027-5","volume":"17","author":"J.A. Bergstra","year":"1982","unstructured":"Bergstra, J.A., Tucker, J.V.: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. Theor. Comput. Sci. 17, 303?315 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"CR8","series-title":"Lecture Notes in Computer Science 115","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/3-540-10843-2_29","volume-title":"International Colloquium on Automata, Languages and Programming 1981","author":"J.A. Bergstra","year":"1981","unstructured":"Bergstra, J.A., Tucker, J.V.: Algebraically specified programming systems and Hoare's logic. In: International Colloquium on Automata, Languages and Programming 1981, Lecture Notes in Computer Science 115. Berlin, Heidelberg, New York: Springer pp. 348?362, 1981"},{"key":"CR9","series-title":"Lecture Notes in Computer Science 131","first-page":"24","volume-title":"Logics of Programs","author":"J.A. Bergstra","year":"1981","unstructured":"Bergstra, J.A., Tucker, J.V.: The refinement of specifications and the stability of Hoare's logic. In: Logics of Programs, Lecture Notes in Computer Science 131. Berlin, Heidelberg, New York: Springer pp. 24?36, 1981"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1016\/0022-0000(82)90013-7","volume":"25","author":"J.A. Bergstra","year":"1982","unstructured":"Bergstra, J.A., Tucker, J.V.: Expressiveness and the completeness of Hoare's logic. J. Comput. Syst. Sci. 25, 276?284 (1982)","journal-title":"J. Comput. Syst. Sci."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0020-0190(82)90095-3","volume":"15","author":"J.A. Bergstra","year":"1982","unstructured":"Bergstra, J.A., Tucker, J.V.: Two theorems about the completeness of Hoare's logic. Information Processing Lett. 15, 143?149 (1982)","journal-title":"Information Processing Lett."},{"key":"CR12","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(83)90107-X","volume":"22","author":"J.A. Bergstra","year":"1983","unstructured":"Bergstra, J.A., Tucker, J.V.: Hoare's logic and Peano's Arithmetic. Theor. Comput. Sci. 22, 265?284 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"CR13","first-page":"213","volume":"28","author":"J.A. Bergstra","year":"1984","unstructured":"Bergstra, J.A., Tucker, J.V.: Hoare's logic for programming languages with two data types. Theor. Comput. Sci. 28, 213?221 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"CR14","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiomatic system for program verification. SIAM J. Comput. 7, 70?90 (1978), Corrigendum 10, 612 (1981)","journal-title":"SIAM J. Comput."},{"key":"CR15","first-page":"181","volume":"5","author":"L. Csirmaz","year":"1981","unstructured":"Csirmaz, L.: On the completeness of proving partial correctness. Acta Cybernet. 5, 181?190 (1981)","journal-title":"Acta Cybernet."},{"key":"CR16","volume-title":"A property of 2-sorted Peano models and program verification","author":"L. Csirmaz","year":"1981","unstructured":"Csirmaz, L., Paris, J.B.: A property of 2-sorted Peano models and program verification. Preprint, Math. Inst., Hungarian Academy, Budapest, 1981"},{"key":"CR17","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 453?457 (1975)","journal-title":"Commun. ACM"},{"key":"CR18","volume-title":"A discipline of programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A discipline of programming. Engelwood Cliffs: Prentice-Hall, 1976"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Mathematical aspects of computer science. J.T. Schwartz (ed.). AMS, pp. 19?32, 1967","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"CR20","first-page":"80","volume-title":"Current trends in programming methodology IV, Data structuring","author":"J.A. Goguen","year":"1978","unstructured":"Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current trends in programming methodology IV, Data structuring. R.T. Yeh (ed.). Englewood Cliffs, New Jersey: Prentice-Hall, pp. 80?149, 1978"},{"key":"CR21","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1145\/357146.357151","volume":"3","author":"I. Greif","year":"1981","unstructured":"Greif, I., Meyer, A.R.: Specifying the semantics of while programs: a tutorial and critique of a paper by Hoare and Lauer. ACM Trans. Progr. Lang. Syst. 3, 484?507 (1981)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"CR22","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming, Commun. ACM 12, 576?580 (1969)","journal-title":"Commun. ACM"},{"key":"CR23","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symposium on the semantics of algorithmic languages","author":"C.A.R. Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Symposium on the semantics of algorithmic languages. E. Engeler (ed.). Berlin, Heidelberg, New York: Springer pp. 102?116, 1971"},{"key":"CR24","first-page":"135","volume":"3","author":"C.A.R. Hoare","year":"1974","unstructured":"Hoare, C.A.R., Lauer, P.: Consistent and complementary formal theories of the semantics of programming languages. Acta Informat. 3, 135?155 (1974)","journal-title":"Acta Informat."},{"key":"CR25","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C.A.R. Hoare","year":"1973","unstructured":"Hoare C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informat. 2, 335?355 (1973)","journal-title":"Acta Informat."},{"key":"CR26","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF00286493","volume":"14","author":"F. Kr\u00f6ger","year":"1980","unstructured":"Kr\u00f6ger, F.: Infinite proof rules for loops. Acta Informat. 14, 371?389 (1980)","journal-title":"Acta Informat."},{"key":"CR27","volume-title":"Ph. D. Thesis","author":"P. Lauer","year":"1972","unstructured":"Lauer, P.: Consistent and complementary formal theories of the semantics of programming languages, Ph. D. Thesis Queens University, Belfast, 1972"},{"key":"CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00260921","volume":"10","author":"R.L. London","year":"1978","unstructured":"London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., Popek, G.L.: Proof rules for the programming language EUCLID. Acta Informat. 10, 1?26 (1978)","journal-title":"Acta Informat."},{"key":"CR29","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0022-0000(69)80009-7","volume":"3","author":"Z. Manna","year":"1969","unstructured":"Manna, Z.: The correctness of programs. J. Comput. Syst. Sci. 3, 119?127 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"CR30","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1070\/RM1961v016n03ABEH001120","volume":"16","author":"A.I. Mal'cev","year":"1961","unstructured":"Mal'cev, A.I.: Constructive algebras I. Russian Math. Surveys 16, 77?129 (1961)","journal-title":"Russian Math. Surveys"},{"key":"CR31","volume-title":"The definition of programming languages","author":"A. McGettrick","year":"1980","unstructured":"McGettrick, A.: The definition of programming languages, Cambridge: University Press, 1980"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/322307.322324","volume":"29","author":"A.R. Meyer","year":"1982","unstructured":"Meyer, A.R., Halpern, J.Y.: Axiomatic definitions of programming languages. A theoretical assessment. J. ACM 29, 555?576 (1982)","journal-title":"J. ACM"},{"key":"CR33","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Halpern, J.Y.: Axiomatic definitions of programming languages II. MIT Lab. Comput. Sci. TM-179 (1980)","DOI":"10.1145\/567446.567466"},{"key":"CR34","volume-title":"Formal specification of programming languages","author":"F.G. Pagan","year":"1981","unstructured":"Pagan, F.G.: Formal specification of programming languages. Englewood Cliffs: Prentice-Hall, 1981"},{"key":"CR35","first-page":"341","volume":"95","author":"M.O. Rabin","year":"1960","unstructured":"Rabin, M.O.: Computable algebra, general theory and the theory of computable fields. Trans. AMS 95, 341?360 (1960)","journal-title":"Trans. AMS"},{"key":"CR36","unstructured":"Schwartz, R.: An axiomatic semantic definition of ALGOL 68. UCLA Computer Science Report 7838, 1978"},{"key":"CR37","unstructured":"Tucker, J.V., Zucker, J.I.: Program correctness over abstract data types, with error state semantics, Monograph (In prep.)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00264252.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00264252\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00264252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T06:59:12Z","timestamp":1585897152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00264252"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984,10]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1984,10]]}},"alternative-id":["BF00264252"],"URL":"https:\/\/doi.org\/10.1007\/bf00264252","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1984,10]]}}}