Hoare-Style Reasoning from Multiple Contracts
Modern software is often developed with advanced mechanisms for code reuse. A software module may build on other software modules or libraries where the source code is not available. And even if the source code is known, the binding mechanism may be such that the binding of methods is not known at verification time, and thus the underlying reused code cannot be determined. For example, in delta- oriented programming the binding of methods depends on the ordering of deltas in each product, making modular reasoning non-trivial. Similar problems occur with traits and subclassing. Reasoning inside a module must then be based on partial knowledge of the methods, typically given by contracts in the form of pairs of pre- and post-conditions, and one may not derive new properties by re-verification of the (unavailable) source code.
In the setting of Hoare logic, this gives some challenges to general rules for adaptation that goes beyond traditional systems for Hoare logic. We develop a novel way of reasoning from multiple contracts, which makes the traditional adaptation rules superfluous. The problem we address does not depend on the choice of programming language. We therefore focus on general rules rather than statement-specific rules. We show soundness and completeness for the suggested rules.
KeywordsHoare logic Multiple contracts Contract-based verification Contract-based specification Adaptation Unavailable source code Soundness Completeness
The authors are indebted to the reviewers for their valuable comments.
- 8.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–60. ACM (2012)Google Scholar
- 21.Owe, O.: Notes on partial correctness. Research Report 26, Department of Informatics, University of Oslo (1977)Google Scholar
- 22.Owe, O.: On practical application of relational calculus. Research Report, Department of Informatics, University of Oslo (1992)Google Scholar
- 29.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–608. Springer, Heidelberg (1996). doi: 10.1007/3-540-60973-3_109 CrossRefGoogle Scholar