Abstract
We sketch a simple theory of Hoare logic contracts for programs with procedures, presented in denotational semantics. In particular, we give a simple semantic justification of the usual procedure-modular treatment of such programs. The justification is given by means of a proof of soundness of a contract-relative denotational semantics against the standard denotational semantics of procedures in the context of procedure declarations. The suggested formal development can be used as an inspiration for more ambitious contract theories.
Access provided by CONRICYT-eBooks. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Rajeev Alur and Swarat Chaudhuri. “Temporal Reasoning for Procedural Programs”. In: Verification, Model Checking and Abstract Interpretation (VMCAI 2010). Vol. 5944. Lecture Notes in Computer Science. Springer, 2010, pp. 45–60.
Krzysztof R. Apt. “Ten Years of Hoare’s Logic: A Survey Part 1”. In: ACM Transactions on Programming Languages and Systems 3.4 (1981), pp. 431–483. https://doi.org/10.1145/357146.357150. URL: http://doi.acm.org/10.1145/357146.357150
E. Cohen et al. “VCC: A Practical System for Verifying Concurrent C”. In: Theorem Proving in Higher Order Logics (TPHOLs 2009). Vol. 5674. Lecture Notes in Computer Science. Springer, 2009, pp. 23–42.
David R. Cok. “OpenJML: JML for Java 7 by Extending OpenJDK”. In: NASA Formal Methods (NFM 2011). Vol. 6617. Lecture Notes in Computer Science. Springer, 2011, pp. 472–479.
C. A. R. Hoare. “An Axiomatic Basis for Computer Programming”. In: Commun. ACM 12.10 (1969), pp. 576–580.
Bertrand Meyer. “Applying “Design by Contract””. In: IEEE Computer 25.10 (1992), pp. 40–51.
Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer Berlin, Heidelberg: SpringerVerlag, 2007. ISBN: 1846286913.
David von Oheimb “Hoare Logic for Mutual Recursion and Local Variables”. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1999). Vol. 1738. Lecture Notes in Computer Science. Springer, 1999, pp. 168–180.
Dimitrios Vytiniotis et al. “HALO: Haskell to logic through denotational semantics”. In: Proceedings of POPL 2013. ACM, 2013, pp. 431–442.
Jonas Westman and Mattias Nyberg. “Conditions of contracts for separating responsibilities in heterogeneous systems”. In: Formal Methods in System Design 52.2 (2018), pp. 147–192.
Jonas Westman et al. “Formal architecture modeling of sequential non-recursive C programs”. In: Science of Computer Programming 146 (2017), pp. 2–27.
Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. Cambridge, MA, USA: MIT Press, 1993. ISBN: 0-262-23169-7.
Acknowledgement
We thank Wolfgang Ahrendt for valuable comments on an earlier draft of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Gurov, D., Westman, J. (2018). A Hoare Logic Contract Theory: An Exercise in Denotational Semantics. In: Müller, P., Schaefer, I. (eds) Principled Software Development. Springer, Cham. https://doi.org/10.1007/978-3-319-98047-8_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-98047-8_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98046-1
Online ISBN: 978-3-319-98047-8
eBook Packages: Computer ScienceComputer Science (R0)