{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:47:44Z","timestamp":1725662864449},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540088608"},{"type":"electronic","value":"9783540358077"}],"license":[{"start":{"date-parts":[[1978,1,1]],"date-time":"1978-01-01T00:00:00Z","timestamp":252460800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1978]]},"DOI":"10.1007\/3-540-08860-1_19","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:33:53Z","timestamp":1330187633000},"page":"251-267","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Semantics and correctness of nondeterministic flowchart programs with recursive procedures"],"prefix":"10.1007","author":[{"given":"Jean H.","family":"Gallier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,26]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Apt, K. R. and De Bakker, J. W., Semantics and proof theory of PASCAL procedures. Automata, Languages and Programming, Lecture Notes in Computer Science, No. 52, Springer Verlag, 1977.","DOI":"10.1007\/3-540-08342-1_3"},{"key":"19_CR2","series-title":"Technical Report","volume-title":"Completeness with finite systems of intermediate assertions for recursive program schemes","author":"K. R. Apt","year":"1977","unstructured":"Apt, K. R. and Meertens, L. G. L. T., Completeness with finite systems of intermediate assertions for recursive program schemes, Technical Report IW 84\/77, Mathematical Center, Amsterdam 1977."},{"key":"19_CR3","first-page":"17","volume":"6","author":"E. A. Ashcroft","year":"1970","unstructured":"Ashcroft, E. A. and Manna, Z., Formalization of properties of parallel programs, Machine Intelligence 6 (1970), 17\u201341, Edinburgh University Press, Edinburgh, Scotland.","journal-title":"Machine Intelligence"},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/3-540-07142-3_71","volume":"25","author":"R. M. Burstall","year":"1975","unstructured":"Burstall, R. M. and Thatcher, J. W., The algebraic theory of recursive program schemes, in Symposium on Category Theory Applied to Computation and Control, Lecture Notes in Computer Science 25 (1975), 126\u2013131.","journal-title":"Lecture Notes in Computer Science"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Programming language constructs for which it is impossible to obtain \"good\" Hoare-like axiom systems, Fourth Annual Symposium on Principles of Programming Languages, Los Angeles, California (January 1977), 10\u201320.","DOI":"10.1145\/512950.512952"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Program invariants as fixed points, Proceedings of the 18th Symposium on Foundations of Computer Science, Providence, Rhode Island (October 1977), 18\u201329.","DOI":"10.1109\/SFCS.1977.25"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1137\/0201006","volume":"1","author":"R. L. Constable","year":"1972","unstructured":"Constable, R. L. and Gries, D., On classes of program schemata, SIAM J. Comput. 1 (1972), 66\u2013118.","journal-title":"SIAM J. Comput."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Courcelle, B. and Nivat, M., Algebraic families of interpretations, Proceedings of the 17th IEEE Symposium on Foundations of Computer Science, Houston, Texas, October 1976, pp. 137\u2013146.","DOI":"10.1109\/SFCS.1976.3"},{"key":"19_CR9","series-title":"Technical Report","volume-title":"Termination of nondeterministic programs","author":"J. W. Bakker De","year":"1975","unstructured":"De Bakker, J. W., Termination of nondeterministic programs, Technical Report IW 50\/75, Mathematical Center, Amsterdam, 1975."},{"issue":"3","key":"19_CR10","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0022-0000(75)80056-0","volume":"11","author":"J. W. Bakker De","year":"1975","unstructured":"De Bakker, J. W. and Meertens, L. G. L. T, On the completeness of the inductive assertion method, J. Comput. System Sci., 11 (1975), No. 3, 323\u2013357.","journal-title":"J. Comput. System Sci."},{"issue":"4","key":"19_CR11","doi-asserted-by":"crossref","first-page":"636","DOI":"10.1145\/321420.321422","volume":"14","author":"R. W. Floyd","year":"1967","unstructured":"Floyd, R. W., Nondeterministic algorithms, J. Assoc. Comput. Mach., 14 (1967), No. 4, 636\u2013644.","journal-title":"J. Assoc. Comput. Mach."},{"key":"19_CR12","unstructured":"Floyd, R. W., Assigning meanings to programs, in Proceedings of a Symposium in Applied Mathematics 19 (1967), Mathematical Aspects of Computer Science (J. T. Schwartz, Ed.), 19\u201332."},{"key":"19_CR13","unstructured":"Gallier, J. H., Semantics and correctness of classes of deterministic and nondeterministic recursive programs, Ph.D. dissertation, U.C.L.A."},{"issue":"3","key":"19_CR14","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1137\/0205030","volume":"5","author":"S. L. Gerhart","year":"1976","unstructured":"Gerhart, S. L, Proof theory of partial correctness verification systems, SIAM J. Comput., 5 (1976), No. 3, 355\u2013377.","journal-title":"SIAM J. Comput."},{"key":"19_CR15","unstructured":"Gorelick, G. A., A complete axiomatic system for proving assertions about recursive and nonrecursive programs, Technical Report No. 75, Department of Computer Science, University of Toronto (1975)."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Greibach, S. A., Theory of program structures: schemes, semantics, verification, Lecture Notes in Computer Science, 36 (1975), Springer Verlag.","DOI":"10.1007\/BFb0023017"},{"key":"19_CR17","series-title":"Semantics and Theory of Computation Report","volume-title":"Correctness of recursive flow diagram programs","author":"J. A. Goguen","year":"1977","unstructured":"Goguen, J. A. and Meseguer, J., Correctness of recursive flow diagram programs, Semantics and Theory of Computation Report No. 8, Computer Science Department, University of California, Los Angeles, July 1977."},{"key":"19_CR18","series-title":"Technical Report","volume-title":"Arithmetical completeness in logics of programs","author":"D. Harel","year":"1977","unstructured":"Harel, D., Arithmetical completeness in logics of programs, Technical Report, Laboratory for Computer Science, MIT, Cambridge, Mass., November 1977."},{"key":"19_CR19","series-title":"Technical Report","volume-title":"Complete axiomatization of properties of recursive programs","author":"D. Harel","year":"1977","unstructured":"Harel, D., Complete axiomatization of properties of recursive programs, Technical Report, Laboratory for Computer Science, MIT, Cambridge, Mass., November 1977."},{"key":"19_CR20","series-title":"Technical Report","volume-title":"On the correctness of regular deterministic programs; a unifying survey","author":"D. Harel","year":"1977","unstructured":"Harel, D., On the correctness of regular deterministic programs; a unifying survey, Technical Report, Laboratory for Computer Science, MIT, Cambridge, Mass., November 1977."},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Harel, D. and Pratt, V. R., Nondeterminism in logics of programs, Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, Tucson, Arizona, January 1978.","DOI":"10.1145\/512760.512782"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Harel, D., Meyer, A. R., and Pratt, V. R., Computability and completeness in logics of programs, Proceedings of the Ninth Annual ACM Symposium on Theory of Computing, Boulder, Colorado, May 1977, pp. 261\u2013268.","DOI":"10.1145\/800105.803416"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A., and Stavi, J., A complete axiomatic system for proving deductions about recursive programs, Proceedings of the Ninth Annual ACM Symposium on Theory of Computing, Boulder, Colorado, May 1977, pp. 249\u2013260.","DOI":"10.1145\/800105.803415"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Lehmann, D., Categories for fixpoint-semantics, Proceedings of the 17th IEEE Symposium on Foundations of Computer Science, Houston, Texas, October 1976, pp. 122\u2013126.","DOI":"10.1109\/SFCS.1976.9"},{"key":"19_CR25","unstructured":"Manna, Z., Mathematical Theory of Computation, McGraw-Hill, 1974."},{"key":"19_CR26","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. System Sci., 3 (1969), 119\u2013127.","journal-title":"J. Comput. System Sci."},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Manna, Z., Mathematical theory of partial correctness, in Symposium on Semantics of Algorithmic Languages (E. Engeler, Ed.), Lecture Notes in Mathematics, 188 (1971), Springer Verlag, 252\u2013269.","DOI":"10.1007\/BFb0059701"},{"key":"19_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(70)90002-0","volume":"1","author":"Z. Manna","year":"1970","unstructured":"Manna, Z., The correctness of nondeterministic programs, Artificial Intelligence, 1 (1970), 1\u201326.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"19_CR29","first-page":"159","volume":"21","author":"Z. Manna","year":"1978","unstructured":"Manna, Z. and Waldinger, R., Is \"sometime\" sometimes better than \"always\"? Intermittent assertions in proving program correctness, Comm. ACM, Vol. 21, No. 2 (1978), 159\u2013172.","journal-title":"Intermittent assertions in proving program correctness, Comm. ACM"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Pratt, V. R., Semantical considerations on Floyd-Hoare Logic, Technical Report MIT\/LCS\/TR-168, MIT, Cambridge, Mass, September 1976.","DOI":"10.1109\/SFCS.1976.27"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-08860-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T23:55:45Z","timestamp":1578527745000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-08860-1_19"}},"subtitle":["Preliminary report"],"short-title":[],"issued":{"date-parts":[[1978]]},"ISBN":["9783540088608","9783540358077"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-08860-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1978]]},"assertion":[{"value":"26 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}