{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T14:25:58Z","timestamp":1649082358922},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2006,11,4]],"date-time":"2006-11-04T00:00:00Z","timestamp":1162598400000},"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":[[2006,11,17]]},"DOI":"10.1007\/s00236-006-0029-5","type":"journal-article","created":{"date-parts":[[2006,11,3]],"date-time":"2006-11-03T09:31:53Z","timestamp":1162546313000},"page":"431-447","source":"Crossref","is-referenced-by-count":0,"title":["Verification conditions are code"],"prefix":"10.1007","volume":"43","author":[{"given":"Andrew M.","family":"Gravell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,11,4]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B Book, Cambridge (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"29_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/390017.808306","volume":"12","author":"A.L. Ambler","year":"1977","unstructured":"Ambler A.L., et\u00a0al. (1977) GYPSY: A language for specification and implementation of verifiable programs. ACM SIGPLAN Notices. 12, 1\u201310","journal-title":"ACM SIGPLAN Notices."},{"key":"29_CR3","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K.R. Apt","year":"1981","unstructured":"Apt K.R. (1981) Ten years of Hoare\u2019s logic. ACM Trans. Program. Lang. Syst. 3, 431\u2013483","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"29_CR4","unstructured":"Back, R.J.R.: On the correctness of refinement steps in program development. Report A-1978\u20131975, University of Helsinki (1978)"},{"key":"29_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.J.R. Back","year":"1998","unstructured":"Back R.J.R., von Wright J. (1998) Refinement Calculus: A Systematic Introduction. Springer, Berlin Heidelberg New York"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Behm, P., et\u00a0al.: Meteor: A Successful Application of B in a Large Project.In: LNCS, vol. 1708, pp. 369\u2013387. Springer, Berlin Heidelberg New York (1999).","DOI":"10.1007\/3-540-48119-2_22"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Butler, M.J., L\u00e5ngbacka.: Program Derivation Using the Refinement Calculator. TPHOLs: 93\u2013108 (1996)","DOI":"10.1007\/BFb0105399"},{"issue":"1","key":"29_CR8","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E.M. Clarke","year":"1979","unstructured":"Clarke E.M. (1979) Programming Language Constructs for which it is impossible to obtain good Hoare axiom systems. JACM 26(1): 129\u2013147","journal-title":"JACM"},{"key":"29_CR9","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook S.A. (1978) Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 70\u201390","journal-title":"SIAM J. Comput."},{"key":"29_CR10","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable R.L. (1986) Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliff"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Crocker D. Safe Object-Oriented Software. In: 12th Critical systems symposium: 19\u201341, Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-0-85729-408-1_2"},{"issue":"5","key":"29_CR12","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R.A. Millo de","year":"1979","unstructured":"de Millo R.A., Lipton R.J., Perlis A.J. (1979) Social processes and proof of theorems and programs. CACM 22(5): 271\u2013280","journal-title":"CACM"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Fetzer, J.H.: Program Verification: the very idea. CACM 31(9), 1048\u20131063","DOI":"10.1145\/48529.48530"},{"key":"29_CR14","unstructured":"Gravell, A.M.: Logical refinement of imperative programs: generating code from verified conditions. (Constraint) Logic Programming and Software Engineering 2000. In: Gupta, G., Ramakrishnan IV (eds.), Imperial College, London (2000)"},{"key":"29_CR15","volume-title":"The Multiple Assignment Statement. LNCS 69, 100\u2013112","author":"D. Gries","year":"1978","unstructured":"Gries D. (1978) The Multiple Assignment Statement. LNCS 69, 100\u2013112. Springer, Heidelberg New York"},{"key":"29_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"Gries D. (1981) The Science of Programming. Springer, Berlin Heidelberg New York"},{"key":"29_CR17","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/69610.357988","volume":"27","author":"ECR. Hehner","year":"1984","unstructured":"Hehner ECR. (1984) predicative programming. I, Commun. ACM 27, 134\u2013143","journal-title":"I, Commun. ACM"},{"key":"29_CR18","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1007\/BF00288466","volume":"23","author":"E.C.R. Hehner","year":"1986","unstructured":"Hehner E.C.R., Gupta L.E., Malton A.J. (1986) predicative methodology. Acta Inform. 23, 487\u2013505","journal-title":"Acta Inform."},{"key":"29_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8596-5","volume-title":"A Practical Theory of Programming","author":"E.C.R. Hehner","year":"1993","unstructured":"Hehner E.C.R. (1993) A Practical Theory of Programming. Springer, Berlin Heidelberg New York"},{"key":"29_CR20","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. (1969) An axiomatic basis of computer programming. Commun. ACM 12, 576\u2013580","journal-title":"Commun. ACM"},{"key":"29_CR21","unstructured":"Hoare C.A.R. Procedures and Parameters: an axiomatic approach. In: Symposium on Semantics of Algorithmic Languages. LNCS 188, 102\u2013116 (1971)"},{"key":"29_CR22","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. (1973) An axiomatic definition of the programming language pascal. Acta Inform 2, 335\u2013355","journal-title":"Acta Inform"},{"key":"29_CR23","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"C.A.R. Hoare","year":"1987","unstructured":"Hoare C.A.R., et\u00a0al. (1987) Laws of Programming. Commun. ACM 30, 672\u2013686","journal-title":"Commun. ACM"},{"key":"29_CR24","volume-title":"Unified Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare C.A.R., He J.(1998) Unified Theories of Programming. Prentice Hall, Englewood cliff"},{"key":"29_CR25","unstructured":"Howard, WA.: The Formulae-as-Types notion of Construction. In: H. B. Curry: Essays on Combinatory logic, lambda calculus and formalism, pp. 479\u2013490 (1980)"},{"issue":"1","key":"29_CR26","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/62029.62030","volume":"21","author":"K. Knight","year":"1989","unstructured":"Knight K. (1989) Unification: a multidisciplinary survey. Comput. Surv. 21(1): 93\u2013124","journal-title":"Comput. Surv."},{"key":"29_CR27","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java Modelling Language. Formal Underpinnings of Java, OOPSLA (1998)"},{"key":"29_CR28","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1990","unstructured":"Morgan C.C. (1990) Programming from Specifications. Prentice Hall, Englewood cliff"},{"issue":"3","key":"29_CR29","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J.M. Morris","year":"1987","unstructured":"Morris J.M. (1987) A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3): 287\u2013306","journal-title":"Sci. Comput. Program."},{"key":"29_CR30","first-page":"63","volume":"6","author":"J.A. Robinson","year":"1971","unstructured":"Robinson J.A. (1971) Computational Logic: the unification computation. Mach. Intell. 6, 63\u201372","journal-title":"Mach. Intell."},{"key":"29_CR31","unstructured":"Rustan, K., Leino, M., Barnett, M., Schulte, W.: The Spec# Programming System: an overview. Microsoft Research (2004)"},{"key":"29_CR32","volume-title":"Logic: A Foundation for Computer Science","author":"V Sperschneider","year":"1991","unstructured":"Sperschneider V, Antoniou G. (1991) Logic: A Foundation for Computer Science. Addison Wesley, Reading"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0029-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-006-0029-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0029-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T09:41:53Z","timestamp":1558690913000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-006-0029-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11,4]]},"references-count":32,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,11,17]]}},"alternative-id":["29"],"URL":"https:\/\/doi.org\/10.1007\/s00236-006-0029-5","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,11,4]]}}}