{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:02:42Z","timestamp":1770753762308,"version":"3.50.0"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319980461","type":"print"},{"value":"9783319980478","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_8","type":"book-chapter","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T21:05:49Z","timestamp":1540328749000},"page":"119-127","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Hoare Logic Contract Theory: An Exercise in Denotational Semantics"],"prefix":"10.1007","author":[{"given":"Dilian","family":"Gurov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonas","family":"Westman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"8_CR1","unstructured":"Rajeev Alur and Swarat Chaudhuri. \u201cTemporal Reasoning for Procedural Programs\u201d. In: Verification, Model Checking and Abstract Interpretation (VMCAI 2010). Vol. 5944. Lecture Notes in Computer Science. Springer, 2010, pp. 45\u201360."},{"issue":"4","key":"8_CR2","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"Krzysztof R. Apt","year":"1981","unstructured":"Krzysztof R. Apt. \u201cTen Years of Hoare\u2019s Logic: A Survey Part 1\u201d. In: ACM Transactions on Programming Languages and Systems 3.4 (1981), pp. 431\u2013483. https:\/\/doi.org\/10.1145\/357146.357150 . URL: http:\/\/doi.acm.org\/10.1145\/357146.357150","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR3","unstructured":"E. Cohen et al. \u201cVCC: A Practical System for Verifying Concurrent C\u201d. In: Theorem Proving in Higher Order Logics (TPHOLs 2009). Vol. 5674. Lecture Notes in Computer Science. Springer, 2009, pp. 23\u201342."},{"key":"8_CR4","unstructured":"David R. Cok. \u201cOpenJML: JML for Java 7 by Extending OpenJDK\u201d. In: NASA Formal Methods (NFM 2011). Vol. 6617. Lecture Notes in Computer Science. Springer, 2011, pp. 472\u2013479."},{"issue":"10","key":"8_CR5","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"C. A. R. Hoare. \u201cAn Axiomatic Basis for Computer Programming\u201d. In: Commun. ACM 12.10 (1969), pp. 576\u2013580.","journal-title":"Communications of the ACM"},{"issue":"10","key":"8_CR6","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Bertrand Meyer. \u201cApplying \u201cDesign by Contract\u201d\u201d. In: IEEE Computer 25.10 (1992), pp. 40\u201351.","journal-title":"Computer"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer Berlin, Heidelberg: SpringerVerlag, 2007. ISBN: 1846286913.","DOI":"10.1007\/978-1-84628-692-6"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"David von Oheimb \u201cHoare Logic for Mutual Recursion and Local Variables\u201d. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1999). Vol. 1738. Lecture Notes in Computer Science. Springer, 1999, pp. 168\u2013180.","DOI":"10.1007\/3-540-46691-6_13"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Dimitrios Vytiniotis et al. \u201cHALO: Haskell to logic through denotational semantics\u201d. In: Proceedings of POPL 2013. ACM, 2013, pp. 431\u2013442.","DOI":"10.1145\/2429069.2429121"},{"key":"8_CR10","unstructured":"Jonas Westman and Mattias Nyberg. \u201cConditions of contracts for separating responsibilities in heterogeneous systems\u201d. In: Formal Methods in System Design 52.2 (2018), pp. 147\u2013192."},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2017.03.007","volume":"146","author":"Jonas Westman","year":"2017","unstructured":"Jonas Westman et al. \u201cFormal architecture modeling of sequential non-recursive C programs\u201d. In: Science of Computer Programming 146 (2017), pp. 2\u201327.","journal-title":"Science of Computer Programming"},{"key":"8_CR12","isbn-type":"print","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"Glynn Winskel","year":"1993","unstructured":"Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. Cambridge, MA, USA: MIT Press, 1993. ISBN: 0-262-23169-7.","ISBN":"https:\/\/id.crossref.org\/isbn\/0262231697"}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T13:14:06Z","timestamp":1572182046000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_8","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}