{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:39:07Z","timestamp":1743043147372,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540092513"},{"type":"electronic","value":"9783540353126"}],"license":[{"start":{"date-parts":[[1979,1,1]],"date-time":"1979-01-01T00:00:00Z","timestamp":283996800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[1979,1,1]],"date-time":"1979-01-01T00:00:00Z","timestamp":283996800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1979]]},"DOI":"10.1007\/bfb0014667","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T05:25:49Z","timestamp":1132723549000},"page":"164-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verification of Euclid programs"],"prefix":"10.1007","author":[{"given":"J. J.","family":"Horning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BF00288660","volume":"6","author":"E. A. Ashcroft","year":"1976","unstructured":"Ashcroft, E. A., M. Clint, and C. A. R. Hoare [1976]. \u201cRemarks on \u2018Program proving: Jumps and functions' by M. Clint and C. A. R. Hoare.\u201d Acta Informatica 6, pp. 317\u2013318.","journal-title":"Acta Informatica"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E. M. Jr. [1977]. \u201cProgramming language constructs for which it is impossible to obtain good Hoare-like axiom systems.\u201d Conference Record, Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 10\u201320.","DOI":"10.1145\/512950.512952"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/BF00288686","volume":"1","author":"M. Clint","year":"1972","unstructured":"Clint, M., and C. A. R. Hoare [1972]. \u201cProgram proving: Jumps and functions.\u201d Acta Informatica 1, pp. 214\u2013224.","journal-title":"Acta Informatica"},{"key":"18_CR4","first-page":"211","volume-title":"Formal Description of Programming Concepts","author":"J. V. Guttag","year":"1978","unstructured":"Guttag, John V., James J. Horning, and Ralph L. London [1978]. \u201cA proof rule for Euclid Procedures.\u201d In Formal Description of Programming Concepts, ed. E. J. Neuhold, pp. 211\u2013220, North-Holland, Amsterdam."},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C. A. R. Hoare","year":"1973","unstructured":"Hoare, C. A. R. and N. Wirth [1973]. \u201cAn axiomatic definition of the programming language Pascal.\u201d Acta Informatica 2, pp. 335\u2013355.","journal-title":"Acta Informatica"},{"issue":"9","key":"18_CR6","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/390014.808286","volume":"8","author":"J. D. Ichbiah","year":"1973","unstructured":"Ichbiah, J. D., J. P. Rissen, and J. C. Heliard [1973]. \u201cThe two-level approach to data definition and space management in the LIS system implementation language.\u201d SIGPLAN Notices 8, no. 9, pp. 79\u201381.","journal-title":"SIGPLAN Notices"},{"key":"18_CR7","first-page":"161","volume-title":"Machine Oriented Higher Level Languages","author":"J. D. Ichbiah","year":"1974","unstructured":"\u2014,\u2014, and \u2014 [1974]. \u201cThe two-level approach to data independent programming in the LIS system implementation language.\u201d In Machine Oriented Higher Level Languages, ed. W. L. van der Poel and L. A. Maarssen, pp. 161\u2013174, North-Holland, Amsterdam."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Lampson, B. W., J. J. Horning, R. L. London, J. G. Mitchell, and G. J. Popek [1977]. \u201cReport on the programming language Euclid.\u201d SIGPLAN Notices 12, no. 2.","DOI":"10.1145\/954666.971189"},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00260921","volume":"10","author":"R. L. London","year":"1978","unstructured":"London, R. L., J. V. Guttag, J. J. Horning, B. W. Lampson, J. G. Mitchell, and G. J. Popek [1978]. \u201cProof rules for the programming language Euclid.\u201d Acta Informatica 10, pp. 1\u201326.","journal-title":"Acta Informatica"},{"key":"18_CR10","unstructured":"Musser, David R. [1977]. \u201cA proof rule for functions.\u201d University of Southern California Information Sciences Institute Technical Report ISI\/RR-77-62."},{"key":"18_CR11","first-page":"339","volume-title":"Proc. IFIP Congress 71","author":"D. L. Parnas","year":"1971","unstructured":"Parnas, D. L. [1971]. \u201cInformation distribution aspects of design methodology.\u201d In Proc. IFIP Congress 71. pp. 339\u2013344, North-Holland, Amsterdam."},{"key":"18_CR12","unstructured":"SIGPLAN [1976]. Special issue on data: abstraction, definition, and structure. SIGPLAN Notices 11."},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/BF00264291","volume":"1","author":"N. Wirth","year":"1971","unstructured":"Wirth, N. [1971]. \u201cThe programming language Pascal.\u201d Acta Informatica 1, pp. 35\u201363.","journal-title":"Acta Informatica"},{"key":"18_CR14","first-page":"3","volume":"7","author":"N. Wirth","year":"1977","unstructured":"\u2014 [1977]. \u201cModula: A language for modular multiprogramming.\u201d Software\u2014Practice and Experience 7, pp. 3\u201335.","journal-title":"Software\u2014Practice and Experience"},{"key":"18_CR15","volume-title":"Pascal\u2014User Manual and Report","author":"N. Wirth","year":"1974","unstructured":"\u2014, and K. Jensen [1974]. Pascal\u2014User Manual and Report, Springer-Verlag, New York."}],"container-title":["Lecture Notes in Computer Science","Program Construction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T21:22:45Z","timestamp":1736112165000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0014667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979]]},"ISBN":["9783540092513","9783540353126"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0014667","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1979]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}