Skip to main content
SpringerLink
Log in

Modular Verification of OO Programs with Interfaces

  • Conference paper
Book cover Formal Methods and Software Engineering (ICFEM 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7635))

Included in the following conference series:

Abstract

Interface types in OO languages support polymorphism, abstraction and information hiding by separating interfaces from their implementations. The separation enhances modularity of programs, however, it causes also challenges to the formal verification. Here we present a study on interface types, and develop a specification and verification theory based on our former veriJ framework. We support multi-specifications for classes inherited from interfaces and the superclass, and keep the verification modularly without re-touching the verified code. The concepts developed in veriJ, namely the abstract specification and specification predicate, play important roles in this extension, and thus are proved widely useful and very natural in the formal proofs of OO programs.

Supported by NNSF of China, Grant No. 90718002 and 61100061.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the spec# experience. Communications of the ACM 54(6), 81–91 (2011)

    Article  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Software: Practice and Experience 35(6), 583–599 (2005)

    Article  Google Scholar 

  4. Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular OO verification with separation logic. In: POPL 2008, pp. 87–99. ACM, New York (2008)

    Chapter  Google Scholar 

  5. Distefano, D., Parkinson, M.J.: jstar: Towards practical verification for java. ACM SIGPLAN Notices 43(10), 213–226 (2008)

    Article  Google Scholar 

  6. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns, Elements of Reusable Object-Oriented Software. Addlison Wesley (1994)

    Google Scholar 

  7. Leavens, G.T.: JML’s Rich, Inherited Specifications for Behavioral Subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 2–34. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Leavens, G.T., Naumann, D.A.: Behavioral subtyping is equivalent to modular reasoning for object-oriented programs. Technical Report 06-36, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (2006)

    Google Scholar 

  9. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. SIGSOFT Software Engineering Notes 31(3), 1–38 (2006)

    Article  Google Scholar 

  10. Leavens, G.T., Müller, P.: Information hiding and visibility in interface specifications. In: 29th International Conference on Software Engineering, ICSE 2007, pp. 385–395 (2007)

    Google Scholar 

  11. Leino, K.R.M.: Toward reliable modular programs. PhD thesis, California Institute of Technology, Pasadena, CA, USA, UMI Order No. GAX95-26835 (1995)

    Google Scholar 

  12. Leino, K.R.M.: Data groups: specifying the modification of extended state. SIGPLAN Notices 33, 144–153 (1998)

    Article  Google Scholar 

  13. Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Transactions on Programing Languages and Systems 16(6), 1811–1841 (1994)

    Article  Google Scholar 

  14. Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  15. Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL 2008, pp. 75–86. ACM, New York (2008)

    Chapter  Google Scholar 

  16. Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Technische Universität München (1997)

    Google Scholar 

  17. Smans, J., Jacobs, B., Piessens, F.: Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148–172. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Yijing, L., Ali, H., Zongyan, Q.: Inheritance and modularity in specification and verification of OO programs. In: TASE 2011, pp. 19–26. IEEE Computer Society (2011)

    Google Scholar 

  19. Yijing, L., Zongyan, Q.: A Separation Logic for OO Programs. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 88–105. Springer, Heidelberg (2010)

    Google Scholar 

  20. Zongyan, Q., Ali, H., Yijing, L.: Modular verification of OO programs with interface types. Technical report, School of Math., Peking Univ. (2012), http://www.mathinst.pku.edu.cn/download.php?classid=22

Download references

Author information

Authors and Affiliations

  1. LMAM and Department of Informatics, School of Math., Peking University, China

    Qiu Zongyan, Hong Ali & Liu Yijing

  2. State Key Laboratory of Computer Science, ISCAS, China

    Qiu Zongyan

Authors
  1. Qiu Zongyan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hong Ali
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Liu Yijing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Japan Advanced Institute of Science and Technology (JAIST), 1-1, Asahidai, 923-1292, Nuomi, Ishikawa, Japan

    Toshiaki Aoki

  2. National Institute of Advanced Industrial Science and Technology (AIST), Nakoji 3-11-46, 661-0974, Amagasaki, Hyogo, Japan

    Kenji Taguchi

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zongyan, Q., Ali, H., Yijing, L. (2012). Modular Verification of OO Programs with Interfaces. In: Aoki, T., Taguchi, K. (eds) Formal Methods and Software Engineering. ICFEM 2012. Lecture Notes in Computer Science, vol 7635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34281-3_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34281-3_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34280-6

  • Online ISBN: 978-3-642-34281-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation