Abstract
Inheritance and method overriding are crucial concepts in object-oriented programming (OOP) languages. These concepts support a hierarchy of classes that reuse common data and methods. Most existing works for OO verification focus on modular reasoning in which they could support dynamic dispatching and thus efficiently enforce the Liskov substitution principle on behavioural subtyping. They are based on \(superclass\ abstraction\) to reason about the correctness of OO programs. However, techniques to reason about the incorrectness of OOP are yet to be investigated.
In this paper, we present a mechanism that 1) specifies the normal and abnormal executions of OO programs by using 
specifications and 
specifications respectively; 2) verifies these specifications by a novel under-approximation proof system based on incorrectness logic that can support dynamic modularity. We introduce subclass reflection with dynamic views and an adapted subtyping relation for under-approximation. Our proposal can deal with both OOP aspects (e.g., behavioural subtyping and casting) and under-approximation aspects (e.g., dropping paths). To demonstrate how the proposed proof system can soundly verify the specifications, we prove its soundness, prototype the proof system, and report on experimental results. The results show that our system can precisely reason about the incorrectness of programs with OOP aspects, such as proving the presence of casting errors and null-pointer-exceptions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
This definition is slightly different from the version in Definition 2 for simplicity.
References
Infer Static Analyzer: Infer. https://fbinfer.com/. Accessed 02 June 2023
Pulse, an interprocedural memory safety analysis. https://github.com/facebook/infer/tree/main/infer/tests/codetoanalyze/java/pulse. Accessed 20 May 2023
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27–56 (2004)
Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular OO verification with separation logic. ACM SIGPLAN Notices 43(1), 87–99 (2008)
Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Prog. 77(9), 1006–1036 (2012)
Cook, W.R., Hill, W., Canning, P.S.: Inheritance is not subtyping. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1990), New York, pp. 125–135. Association for Computing Machinery (1989)
Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering (ICSE 1996), pp. 258–267. IEEE Computer Society (1996)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271–281 (1972)
Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46428-X_20
Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_19
Le, Q.L., Raad, A., Villard, J., Berdine, J., Dreyer, D., O’Hearn, P.W.: Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6(OOPSLA1) (2022)
Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 41–60. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_3
Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. ACM Trans. Prog. Lang. Syst. 37(4), 1–88 (2015)
Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8), 705–778 (1995)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24851-4_22
Li, W., Le, Q.L., Song, Y., Chin, W.-N.: Incorrectness proofs for object-oriented programs via subclass reflection (technical report). https://www.comp.nus.edu.sg/~yahuis/APLAS2023.pdf (2023)
Liskov, B.: Keynote address-data abstraction and hierarchy. In: Addendum to the Proceedings on Object-Oriented Programming Systems, Languages and Applications (Addendum), pp. 17–34 (1987)
Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)
Long, F., Amidon, P., Rinard, M.: Automatic inference of code transforms for patch generation. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pp. 727–739 (2017)
Luo, C., Qin, S.: Separation logic for multiple inheritance. Electron. Notes Theor. Comput. Sci. 212, 27–40 (2008)
Madeiral, F., Urli, S., Maia, M., Monperrus, M.: Bears: an extensible java bug benchmark for automatic program repair studies. In: 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER), pp. 468–478. IEEE (2019)
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1
O’Hearn, P.W.: Incorrectness logic. Proc. ACM Prog. Lang. 4(POPL), 10:1–10:32 (2020)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 247–258 (2005)
Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. ACM SIGPLAN Notices 43(1), 75–86 (2008)
Raad, A., Berdine, J., Dang, H.-H., Dreyer, D., O’Hearn, P., Villard, J.: Local reasoning about the presence of bugs: incorrectness separation Logic. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 225–252. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_14
Sadowski, C., Aftandilian, E., Eagle, A., Miller-Cushon, L., Jaspan, C.: Lessons from building static analysis tools at google. Commun. ACM 61(4), 58–66 (2018)
Tomassi, D.A., et al.: Bugswarm: mining and continuously growing a dataset of reproducible failures and fixes. In: 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE), pp. 339–349. IEEE (2019)
van Tonder, R., Le Goues, C.: Static automated program repair for heap properties. In: Proceedings of the 40th International Conference on Software Engineering, pp. 151–162 (2018)
de Vries, E., Koutavas, V.: Reverse hoare logic. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 155–171. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_12
Acknowledgements
The authors would like to thank anonymous reviewers for their comments. This work was partially supported by a Singapore Ministry of Education (MoE) Tier3 grant “Automated Program Repair”, MOE-MOET32021-0001.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Li, W., Le, Q.L., Song, Y., Chin, WN. (2023). Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection. In: Hur, CK. (eds) Programming Languages and Systems. APLAS 2023. Lecture Notes in Computer Science, vol 14405. Springer, Singapore. https://doi.org/10.1007/978-981-99-8311-7_13
Download citation
DOI: https://doi.org/10.1007/978-981-99-8311-7_13
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-99-8310-0
Online ISBN: 978-981-99-8311-7
eBook Packages: Computer ScienceComputer Science (R0)