Abstract
When developing complex software and systems, contracts 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 contract theories 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, contract meta-theories 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. [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’s design-by-contract methodology [18]. At the core of this gap appears to be the notion of procedure: 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.
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 denotational semantics. We show that, on the one hand, the specification of contracts of procedures in Hoare logic, 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.
This work has been funded by the Swedish Governmental Agency for Innovation Systems (VINNOVA) under the AVerT project 2018-02727.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (Jan 1993). https://doi.org/10.1145/151646.151649
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–58 (2012). https://doi.org/10.1007/978-3-642-28872-2_3
Bekić, H.: Definable operation in general algebras, and the theory of automata and flowcharts. In: Programming Languages and Their Definition - Hans Bekić (1936-1982). Lecture Notes in Computer Science, vol. 177, pp. 30–55. Springer (1984). https://doi.org/10.1007/BFb0048939
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. 5382, pp. 200–225 (10 2007). https://doi.org/10.1007/978-3-540-92188-2_9
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. 12. Now Publishers (2018). https://doi.org/10.1561/1000000053
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–147 (09 2008). https://doi.org/10.1109/FDL.2008.4641436
Bubel, R., Hähnle, R., Pelevina, M.: Fully abstract operation contracts. In: Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. pp. 120–134 (2014). https://doi.org/10.1007/978-3-662-45231-8_9
Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.: A compositional specification theory for component behaviours. In: Programming Languages and Systems. pp. 148–168. Springer Berlin Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_8
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
Floyd, R.W.: Assigning meanings to programs. Mathematical aspects of computer science 19, 19–32 (1967). https://doi.org/10.1007/978-94-011-1793-7_4
Gurov, D., Lidström, 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–18. Springer (2017). https://doi.org/10.1007/978-3-319-67113-0_1
Gurov, D., Westman, J.: A Hoare Logic Contract Theory: An Exercise in Denotational Semantics, pp. 119–127. Springer International Publishing, Cham (2018). https://doi.org/10.1007/978-3-319-98047-8_8
Hähnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Automated Deduction – CADE-24. vol. 7898, pp. 300–314 (06 2013). https://doi.org/10.1007/978-3-642-38574-2_21
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3) (Jun 2012). https://doi.org/10.1145/2187671.2187678
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (Oct 1969). https://doi.org/10.1145/363235.363259
Jones, C.: Specification and design of (parallel) programs. In: Proceedings Of IFIP’83. vol. 83, pp. 321–332 (01 1983)
Lidström, C., Gurov, D.: An abstract contract theory for programs with procedures (full version). CoRR abs/2101.06087 (2021), https://arxiv.org/abs/2101.06087
Meyer, B.: Applying "design by contract". IEEE Computer 25(10), 40–51 (1992). https://doi.org/10.1109/2.161279
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
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–365. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-61467-6_22
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–278. Springer (2017). https://doi.org/10.1007/978-3-319-66845-1_17
van Staden, S.: On rely-guarantee reasoning. In: Mathematics of Program Construction. pp. 30–49. Springer International Publishing, Cham (2015). https://doi.org/10.1007/978-3-319-19797-5_2
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Lidström, C., Gurov, D. (2021). An Abstract Contract Theory for Programs with Procedures. In: Guerra, E., Stoelinga, M. (eds) Fundamental Approaches to Software Engineering. FASE 2021. Lecture Notes in Computer Science(), vol 12649. Springer, Cham. https://doi.org/10.1007/978-3-030-71500-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-71500-7_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71499-4
Online ISBN: 978-3-030-71500-7
eBook Packages: Computer ScienceComputer Science (R0)