{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:38:57Z","timestamp":1743071937397,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030714994"},{"type":"electronic","value":"9783030715007"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>When developing complex software and systems, <jats:italic>contracts<\/jats:italic> provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hierarchical fashion. In specific application areas, dedicated <jats:italic>contract theories<\/jats:italic> formalise the notion of contract and the operations on contracts in a manner that supports best the development of systems in that area. At the other end, <jats:italic>contract meta-theories<\/jats:italic> attempt to provide a systematic view on the various contract theories by axiomatising their desired properties. However, there exists a noticeable gap between the most well-known contract meta-theory of Benveniste et al.\u00a0[5], which focuses on the design of embedded and cyber-physical systems, and the established way of using contracts when developing general software, following Meyer\u2019s design-by-contract methodology\u00a0[18]. At the core of this gap appears to be the notion of <jats:italic>procedure<\/jats:italic>: while it is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components.<\/jats:p><jats:p>In this paper, we provide a first step towards a contract theory that takes procedures as the basic building block, and is at the same time an instantiation of the meta-theory. To this end, we propose an abstract contract theory for sequential programming languages with procedures, based on <jats:italic>denotational semantics<\/jats:italic>. We show that, on the one hand, the specification of contracts of procedures in <jats:italic>Hoare logic<\/jats:italic>, and their procedure-modular verification, can be cast naturally in the framework of our abstract contract theory. On the other hand, we also show our contract theory to fulfil the axioms of the meta-theory. In this way, we give further evidence for the utility of the meta-theory, and prepare the ground for combining our instantiation with other, already existing instantiations.<\/jats:p>","DOI":"10.1007\/978-3-030-71500-7_8","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T13:12:14Z","timestamp":1616159534000},"page":"152-171","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["An Abstract Contract Theory for Programs with Procedures"],"prefix":"10.1007","author":[{"given":"Christian","family":"Lidstr\u00f6m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73\u2013132 (Jan 1993). https:\/\/doi.org\/10.1145\/151646.151649","DOI":"10.1145\/151646.151649"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Bauer, S., David, A., Hennicker, R., Larsen, K., Legay, A., Nyman, U., Wasowski, A.: Moving from specifications to contracts in component-based design. In: Fundamental Approaches to Software Engineering. pp. 43\u201358 (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_3","DOI":"10.1007\/978-3-642-28872-2_3"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Beki\u0107, H.: Definable operation in general algebras, and the theory of automata and flowcharts. In: Programming Languages and Their Definition - Hans Beki\u0107 (1936-1982). Lecture Notes in Computer Science, vol.\u00a0177, pp. 30\u201355. Springer (1984). https:\/\/doi.org\/10.1007\/BFb0048939","DOI":"10.1007\/BFb0048939"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: Formal Methods for Components and Objects. vol.\u00a05382, pp. 200\u2013225 (10 2007). https:\/\/doi.org\/10.1007\/978-3-540-92188-2_9","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for System Design, vol.\u00a012. Now Publishers (2018). https:\/\/doi.org\/10.1561\/1000000053","DOI":"10.1561\/1000000053"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Benvenuti, L., Ferrari, A., Mangeruca, L., Mazzi, E., Passerone, R., Sofronis, C.: A contract-based formalism for the specification of heterogeneous systems. In: 2008 Forum on Specification, Verification and Design Languages. pp. 142\u2013147 (09 2008). https:\/\/doi.org\/10.1109\/FDL.2008.4641436","DOI":"10.1109\/FDL.2008.4641436"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Bubel, R., H\u00e4hnle, R., Pelevina, M.: Fully abstract operation contracts. In: Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. pp. 120\u2013134 (2014). https:\/\/doi.org\/10.1007\/978-3-662-45231-8_9","DOI":"10.1007\/978-3-662-45231-8_9"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.: A compositional specification theory for component behaviours. In: Programming Languages and Systems. pp. 148\u2013168. Springer Berlin Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_8","DOI":"10.1007\/978-3-642-28869-2_8"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Science of Computer Programming 97 (2015). https:\/\/doi.org\/10.1016\/j.scico.2014.06.011","DOI":"10.1016\/j.scico.2014.06.011"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Floyd, R.W.: Assigning meanings to programs. Mathematical aspects of computer science 19, 19\u201332 (1967). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Gurov, D., Lidstr\u00f6m, C., Nyberg, M., Westman, J.: Deductive functional verification of safety-critical embedded c-code: An experience report. In: Proceedings of FMICS-AVoCS 2017. Lecture Notes in Computer Science, vol. 10471, pp. 3\u201318. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67113-0_1","DOI":"10.1007\/978-3-319-67113-0_1"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Gurov, D., Westman, J.: A Hoare Logic Contract Theory: An Exercise in Denotational Semantics, pp. 119\u2013127. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98047-8_8","DOI":"10.1007\/978-3-319-98047-8_8"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Automated Deduction \u2013 CADE-24. vol.\u00a07898, pp. 300\u2013314 (06 2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_21","DOI":"10.1007\/978-3-642-38574-2_21"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3) (Jun 2012). https:\/\/doi.org\/10.1145\/2187671.2187678","DOI":"10.1145\/2187671.2187678"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (Oct 1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"8_CR16","unstructured":"Jones, C.: Specification and design of (parallel) programs. In: Proceedings Of IFIP\u201983. vol.\u00a083, pp. 321\u2013332 (01 1983)"},{"key":"8_CR17","unstructured":"Lidstr\u00f6m, C., Gurov, D.: An abstract contract theory for programs with procedures (full version). CoRR abs\/2101.06087 (2021), https:\/\/arxiv.org\/abs\/2101.06087"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Meyer, B.: Applying \"design by contract\". IEEE Computer 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","DOI":"10.1109\/2.161279"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Springer-Verlag, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-1-84628-692-6","DOI":"10.1007\/978-1-84628-692-6"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Nyberg, M., Westman, J., Gurov, D.: Formally proving compositionality in industrial systems with informal specifications. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications. pp. 348\u2013365. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_22","DOI":"10.1007\/978-3-030-61467-6_22"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Owe, O., Ramezanifarkhani, T., Fazeldehkordi, E.: Hoare-style reasoning from multiple contracts. In: Integrated Formal Methods - 13th International Conference. Lecture Notes in Computer Science, vol. 10510, pp. 263\u2013278. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_17","DOI":"10.1007\/978-3-319-66845-1_17"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"van Staden, S.: On rely-guarantee reasoning. In: Mathematics of Program Construction. pp. 30\u201349. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19797-5_2","DOI":"10.1007\/978-3-319-19797-5_2"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, USA (1993). https:\/\/doi.org\/10.7551\/mitpress\/3054.001.0001","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71500-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:16:26Z","timestamp":1616199386000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71500-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030714994","9783030715007"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71500-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"52","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}