{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:49Z","timestamp":1740098929568,"version":"3.37.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_17","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"263-278","source":"Crossref","is-referenced-by-count":2,"title":["Hoare-Style Reasoning from Multiple Contracts"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Owe","sequence":"first","affiliation":[]},{"given":"Toktam","family":"Ramezanifarkhani","sequence":"additional","affiliation":[]},{"given":"Elahe","family":"Fazeldehkordi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"issue":"4","key":"17_CR1","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey - part I. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/3-540-60117-1_8","volume-title":"Mathematics of Program Construction","author":"R-J Back","year":"1995","unstructured":"Back, R.-J., Butler, M.: Exploring summation and product operators in the refinement calculus. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 128\u2013158. Springer, Heidelberg (1995). doi:\n10.1007\/3-540-60117-1_8"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005). doi:\n10.1007\/978-3-540-30569-9_3"},{"key":"17_CR4","volume-title":"Verification of Object-oriented Software: The KeY Approach","author":"B Beckert","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: Verification of Object-oriented Software: The KeY Approach. Springer, Heidelberg (2007)"},{"issue":"5","key":"17_CR5","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF00289144","volume":"26","author":"A Bijlsma","year":"1989","unstructured":"Bijlsma, A., Matthews, P.A., Wiltink, J.G.: A sharp proof rule for procedures in WP semantics. Acta Inform. 26(5), 409\u2013419 (1989)","journal-title":"Acta Inform."},{"issue":"1","key":"17_CR6","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"SA Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70\u201390 (1978)","journal-title":"SIAM J. Comput."},{"key":"17_CR7","series-title":"International Series in Computer Science","volume-title":"Verifiable Programming","author":"O-J Dahl","year":"1992","unstructured":"Dahl, O.-J.: Verifiable Programming. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1992)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Damiani, F., Dovland, J., Johnsen, E.B., Owe, O., Schaefer, I., Yu, I.C.: A transformational proof system for delta-oriented programming. In: Proceedings of the 16th International Software Product Line Conference, vol. 2 (SPLC 2012), pp. 53\u201360. ACM (2012)","DOI":"10.1145\/2364412.2364422"},{"issue":"5\u20136","key":"17_CR9","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1016\/j.jlamp.2014.03.003","volume":"83","author":"CC Din","year":"2014","unstructured":"Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. J. Log. Algebr. Methods Program. 83(5\u20136), 360\u2013383 (2014)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"7","key":"17_CR10","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1016\/j.jlap.2010.07.008","volume":"79","author":"J Dovland","year":"2010","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Log. Algebr. Program. 79(7), 578\u2013607 (2010)","journal-title":"J. Log. Algebr. Program."},{"issue":"10","key":"17_CR11","doi-asserted-by":"crossref","first-page":"915","DOI":"10.1016\/j.scico.2010.09.006","volume":"76","author":"J Dovland","year":"2011","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Sci. Comput. Program. 76(10), 915\u2013941 (2011)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"17_CR12","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/1119479.1119483","volume":"28","author":"S Ducasse","year":"2006","unstructured":"Ducasse, S., Nierstrasz, O., Sch\u00e4rli, N., Wuyts, R., Black, A.P.: Traits: a mechanism for fine-grained reuse. ACM Trans. Program. Lang. Syst. 28(2), 331\u2013388 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"17_CR13","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/S1571-0661(05)80486-4","volume":"70","author":"L Groves","year":"2002","unstructured":"Groves, L.: Refinement and the Z schema calculus. Electron. Notes Theor. Comput. Sci. 70(3), 70\u201393 (2002). REFINE 2002 (The BCS FACS Refinement Workshop)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-38574-2_21","volume-title":"Automated Deduction \u2013 CADE-24","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 300\u2013314. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-38574-2_21"},{"issue":"10","key":"17_CR15","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"17_CR16","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symposium on Semantics of Algorithmic Languages","author":"CAR Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 102\u2013116. Springer, Heidelberg (1971). doi:\n10.1007\/BFb0059696"},{"issue":"1","key":"17_CR17","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/s001650050037","volume":"11","author":"BP Mahony","year":"1999","unstructured":"Mahony, B.P.: The least conjunctive refinement and promotion in the refinement calculus. Formal Aspects Comput. 11(1), 75\u2013105 (1999)","journal-title":"Formal Aspects Comput."},{"issue":"10","key":"17_CR18","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"17_CR19","volume-title":"Eiffel: The Language","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: The Language. Prentice Hall, Englewood Cliffs (1992)"},{"issue":"3","key":"17_CR20","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/0304-3975(83)90009-9","volume":"24","author":"E-R Olderog","year":"1983","unstructured":"Olderog, E.-R.: On the notion of expressiveness and the rule of adaptation. Theoret. Comput. Sci. 24(3), 337\u2013347 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR21","unstructured":"Owe, O.: Notes on partial correctness. Research Report 26, Department of Informatics, University of Oslo (1977)"},{"key":"17_CR22","unstructured":"Owe, O.: On practical application of relational calculus. Research Report, Department of Informatics, University of Oslo (1992)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-540-27815-3_31","volume-title":"Algebraic Methodology and Software Technology","author":"C Pierik","year":"2004","unstructured":"Pierik, C., de Boer, F.S.: Modularity and the rule of adaptation. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 394\u2013408. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-27815-3_31"},{"issue":"2","key":"17_CR24","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/BF02745521","volume":"21","author":"W Reif","year":"1996","unstructured":"Reif, W., Stenzel, K.: Reuse of proofs in software verification. Sadhana 21(2), 229\u2013244 (1996)","journal-title":"Sadhana"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15579-6_6","volume-title":"Software Product Lines: Going Beyond","author":"I Schaefer","year":"2010","unstructured":"Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol. 6287, pp. 77\u201391. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-15579-6_6"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-45719-4_30","volume-title":"Algebraic Methodology and Software Technology","author":"A Schairer","year":"2002","unstructured":"Schairer, A., Hutter, D.: Proof transformations for evolutionary formal software development. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 441\u2013456. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45719-4_30"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-540-45070-2_12","volume-title":"ECOOP 2003 \u2013 Object-Oriented Programming","author":"N Sch\u00e4rli","year":"2003","unstructured":"Sch\u00e4rli, N., Ducasse, S., Nierstrasz, O., Black, A.P.: Traits: composable units of behaviour. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 248\u2013274. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-45070-2_12"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0024672","volume-title":"FME \u201993: Industrial-Strength Formal Methods","author":"N Ward","year":"1993","unstructured":"Ward, N.: Adding specification constructors to the refinement calculus. In: Woodcock, J.C.P., Larsen, P.G. (eds.) FME 1993. LNCS, vol. 670, pp. 652\u2013670. Springer, Heidelberg (1993). doi:\n10.1007\/BFb0024672"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/3-540-60973-3_109","volume-title":"FME\u201996: Industrial Benefit and Advances in Formal Methods","author":"J Zwiers","year":"1996","unstructured":"Zwiers, J., Hannemann, U., Lakhneche, Y., Stomp, F., de Roever, W.-P.: Modular completeness: integrating the reuse of specified software in top-down program development. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 595\u2013608. Springer, Heidelberg (1996). doi:\n10.1007\/3-540-60973-3_109"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:42:28Z","timestamp":1503747748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}