Advertisement

Hoare-Style Reasoning from Multiple Contracts

  • Olaf OweEmail author
  • Toktam RamezanifarkhaniEmail author
  • Elahe FazeldehkordiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

Abstract

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.

Keywords

Hoare logic Multiple contracts Contract-based verification Contract-based specification Adaptation Unavailable source code Soundness Completeness 

Notes

Acknowledgment

The authors are indebted to the reviewers for their valuable comments.

References

  1. 1.
    Apt, K.R.: Ten years of Hoare’s logic: a survey - part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefzbMATHGoogle Scholar
  2. 2.
    Back, R.-J., Butler, M.: Exploring summation and product operators in the refinement calculus. In: Möller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 128–158. Springer, Heidelberg (1995). doi: 10.1007/3-540-60117-1_8 CrossRefGoogle Scholar
  3. 3.
    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–69. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-30569-9_3 CrossRefGoogle Scholar
  4. 4.
    Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of Object-oriented Software: The KeY Approach. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  5. 5.
    Bijlsma, A., Matthews, P.A., Wiltink, J.G.: A sharp proof rule for procedures in WP semantics. Acta Inform. 26(5), 409–419 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70–90 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Dahl, O.-J.: Verifiable Programming. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1992)zbMATHGoogle Scholar
  8. 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
  9. 9.
    Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. J. Log. Algebr. Methods Program. 83(5–6), 360–383 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Log. Algebr. Program. 79(7), 578–607 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Sci. Comput. Program. 76(10), 915–941 (2011)CrossRefzbMATHGoogle Scholar
  12. 12.
    Ducasse, S., Nierstrasz, O., Schärli, N., Wuyts, R., Black, A.P.: Traits: a mechanism for fine-grained reuse. ACM Trans. Program. Lang. Syst. 28(2), 331–388 (2006)CrossRefGoogle Scholar
  13. 13.
    Groves, L.: Refinement and the Z schema calculus. Electron. Notes Theor. Comput. Sci. 70(3), 70–93 (2002). REFINE 2002 (The BCS FACS Refinement Workshop)CrossRefzbMATHGoogle Scholar
  14. 14.
    Hähnle, 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–314. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38574-2_21 CrossRefGoogle Scholar
  15. 15.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefzbMATHGoogle Scholar
  16. 16.
    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–116. Springer, Heidelberg (1971). doi: 10.1007/BFb0059696 CrossRefGoogle Scholar
  17. 17.
    Mahony, B.P.: The least conjunctive refinement and promotion in the refinement calculus. Formal Aspects Comput. 11(1), 75–105 (1999)CrossRefzbMATHGoogle Scholar
  18. 18.
    Meyer, B.: Applying “design by contract”. IEEE Comput. 25(10), 40–51 (1992)CrossRefGoogle Scholar
  19. 19.
    Meyer, B.: Eiffel: The Language. Prentice Hall, Englewood Cliffs (1992)zbMATHGoogle Scholar
  20. 20.
    Olderog, E.-R.: On the notion of expressiveness and the rule of adaptation. Theoret. Comput. Sci. 24(3), 337–347 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Owe, O.: Notes on partial correctness. Research Report 26, Department of Informatics, University of Oslo (1977)Google Scholar
  22. 22.
    Owe, O.: On practical application of relational calculus. Research Report, Department of Informatics, University of Oslo (1992)Google Scholar
  23. 23.
    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–408. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27815-3_31 CrossRefGoogle Scholar
  24. 24.
    Reif, W., Stenzel, K.: Reuse of proofs in software verification. Sadhana 21(2), 229–244 (1996)CrossRefzbMATHGoogle Scholar
  25. 25.
    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–91. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-15579-6_6 CrossRefGoogle Scholar
  26. 26.
    Schairer, A., Hutter, D.: Proof transformations for evolutionary formal software development. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 441–456. Springer, Heidelberg (2002). doi: 10.1007/3-540-45719-4_30 CrossRefGoogle Scholar
  27. 27.
    Schärli, N., Ducasse, S., Nierstrasz, O., Black, A.P.: Traits: composable units of behaviour. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 248–274. Springer, Heidelberg (2003). doi: 10.1007/978-3-540-45070-2_12 CrossRefGoogle Scholar
  28. 28.
    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–670. Springer, Heidelberg (1993). doi: 10.1007/BFb0024672 CrossRefGoogle Scholar
  29. 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

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Department of InformaticsUniversity of OsloOsloNorway

Personalised recommendations