{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:16:47Z","timestamp":1770977807478,"version":"3.50.1"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T00:00:00Z","timestamp":1710892800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2024,3,31]]},"abstract":"<jats:p>Class invariants\u2014consistency constraints preserved by every operation on objects of a given type\u2014are fundamental to building, understanding, and verifying object-oriented programs. For verification, however, they raise difficulties, which have not yet received a generally accepted solution. The present work introduces a proof rule meant to address these issues and allow verification tools to benefit from invariants.<\/jats:p>\n          <jats:p>It clarifies the notion of invariant and identifies the three associated problems: callbacks, furtive access, and reference leak. As an example, the 2016 Ethereum DAO bug, in which $50 million was stolen, resulted from a callback invalidating an invariant.<\/jats:p>\n          <jats:p>The discussion starts with a simplified model of computation and an associated proof rule, demonstrating its soundness. It then removes one by one the three simplifying assumptions, each removal raising one of the three issues and leading to a corresponding adaptation to the proof rule. The final version of the rule can tackle tricky examples, including \u201cchallenge problems\u201d listed in the literature.<\/jats:p>","DOI":"10.1145\/3626201","type":"journal-article","created":{"date-parts":[[2024,1,24]],"date-time":"2024-01-24T12:17:00Z","timestamp":1706098620000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["The Concept of Class Invariant in Object-oriented Programming"],"prefix":"10.1145","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5985-7434","authenticated-orcid":false,"given":"Bertrand","family":"Meyer","sequence":"first","affiliation":[{"name":"Constructor Institute, Schaffhausen, Switzerland and Eiffel Software, Santa Barbara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4186-066X","authenticated-orcid":false,"given":"Alisa","family":"Arkadova","sequence":"additional","affiliation":[{"name":"Previously at University of Toulouse, Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4873-8306","authenticated-orcid":false,"given":"Alexander","family":"Kogtenkov","sequence":"additional","affiliation":[{"name":"Previously at Constructor Institute, Schaffhausen, Switzerland and Previously at Eiffel Software, Santa Barbara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-030-54994-7_24","volume-title":"Formal Methods. FM 2019 International Workshops","author":"Aiello M. Anthony","year":"2020","unstructured":"M. Anthony Aiello, Johannes Kanig, and Taro Kurita. 2020. Call me back, I have a type invariant. In Formal Methods. FM 2019 International Workshops. Springer, 325\u2013336."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428277"},{"key":"e_1_3_2_4_2","unstructured":"Alisa Arkadova Alexander Kogtenkov Alexandr Naumchev and Bertrand Meyer. 2021-2022. Source Code and Other Supporting Material for This Article. Retrieved from https:\/\/github.com\/alicealice19\/invariant_paper"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1707790.1707794"},{"key":"e_1_3_2_6_2","first-page":"358","volume-title":"ECOOP \u201911","author":"Balzer Stephanie","year":"2011","unstructured":"Stephanie Balzer and Thomas R. Gross. 2011. Verifying multi-object invariants with relationships. In ECOOP \u201911, Mira Mezini (Ed.), Vol. 6813. Springer, 358\u2013382."},{"issue":"3","key":"e_1_3_2_7_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2485982","article-title":"Local reasoning for global invariants, part II: Dynamic boundaries","volume":"60","author":"Banerjee Anindya","year":"2013","unstructured":"Anindya Banerjee and David A. Naumann. 2013. Local reasoning for global invariants, part II: Dynamic boundaries. J. ACM 60, 3 (June2013), 1\u201373.","journal-title":"J. ACM"},{"key":"e_1_3_2_8_2","first-page":"387","volume-title":"ECOOP \u201908","author":"Banerjee Anindya","year":"2008","unstructured":"Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2008. Regional logic for local reasoning about global invariants. In ECOOP \u201908, Jan Vitek (Ed.), Vol. 5142. Springer, 387\u2013411."},{"issue":"3","key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2485982","article-title":"Local reasoning for global invariants, part I: Region logic","volume":"60","author":"Banerjee Anindya","year":"2013","unstructured":"Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2013. Local reasoning for global invariants, part I: Region logic. J. ACM 60, 3 (June2013), 1\u201356.","journal-title":"J. ACM"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98047-8_2"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_3_2_12_2","first-page":"49","volume-title":"CASSIS \u201904","author":"Barnett Mike","year":"2004","unstructured":"Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. 2004. The Spec# programming system: An overview. In CASSIS \u201904. Springer, 49\u201369."},{"key":"e_1_3_2_13_2","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"Barnett Mike","year":"2004","unstructured":"Mike Barnett and David A. Naumann. 2004. Friends need a bit more: Maintaining invariants over shared state. In Mathematics of Program Construction, Dexter Kozen (Ed.). Springer, 54\u201384."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10431-7_6"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1007\/978-3-642-14295-6_42","volume-title":"Computer Aided Verification","author":"Cohen Ernie","year":"2010","unstructured":"Ernie Cohen, Micha\u0142 Moskal, Wolfram Schulte, and Stephan Tobies. 2010. Local verification of global invariants in concurrent programs. In Computer Aided Verification, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer, 480\u2013494."},{"key":"e_1_3_2_17_2","unstructured":"Phil Daian. 2016. Analysis of the DAO Exploit. Retrieved from https:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/"},{"key":"e_1_3_2_18_2","first-page":"412","volume-title":"ECOOP \u201908","author":"Drossopoulou S.","year":"2008","unstructured":"S. Drossopoulou, A. Francalanza, P. M\u00fcller, and A. J. Summers. 2008. A unified framework for verification techniques for object invariants. In ECOOP \u201908, Jan Vitek (Ed.), Vol. 5142. Springer, 412\u2013437."},{"key":"e_1_3_2_19_2","unstructured":"Eiffel Software. Concurrent Programming with SCOOP. Retrieved from https:\/\/www.eiffel.org\/doc\/solutions\/Concurrent_programming_with_SCOOP"},{"issue":"19","key":"e_1_3_2_20_2","first-page":"1","article-title":"Assigning meanings to programs","volume":"19","author":"Floyd Robert W.","year":"1967","unstructured":"Robert W. Floyd. 1967. Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19-32 (1967), 1.","journal-title":"Math. Aspects Comput. Sci."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2506375"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0419-0"},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/978-3-540-89247-2_10","volume-title":"Runtime Verification","author":"Gopinathan Madhu","year":"2008","unstructured":"Madhu Gopinathan and Sriram K. Rajamani. 2008. Runtime monitoring of object invariants with guarantee. In Runtime Verification, Martin Leucker (Ed.), Vol. 5289. Springer, 158\u2013172."},{"key":"e_1_3_2_24_2","first-page":"43","volume-title":"ISSTA \u201908\u2013WODA \u201908","author":"Gorbovitski Michael","year":"2008","unstructured":"Michael Gorbovitski, Tom Rothamel, Yanhong A. Liu, and Scott D. Stoller. 2008. Efficient runtime invariant checking: A framework and case study. In ISSTA \u201908\u2013WODA \u201908. ACM Press, 43."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symposium on Semantics of Algorithmic Languages","author":"Hoare C. A. R.","year":"1971","unstructured":"C. A. R. Hoare. 1971. Procedures and parameters: An axiomatic approach. In Symposium on Semantics of Algorithmic Languages, E. Engeler (Ed.), Vol. 188. Springer, 102\u2013116."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46428-X_15"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/978-3-319-10431-7_25","volume-title":"Software Engineering and Formal Methods","author":"Huster Stefan","year":"2014","unstructured":"Stefan Huster, Patrick Heckeler, Hanno Eichelberger, J\u00fcrgen Ruf, Sebastian Burg, Thomas Kropf, and Wolfgang Rosenstiel. 2014. More flexible object invariants with less specification overhead. In Software Engineering and Formal Methods, Dimitra Giannakopoulou and Gwen Sala\u00fcn (Eds.), Vol. 8702. Springer, 302\u2013316."},{"key":"e_1_3_2_31_2","first-page":"137","volume-title":"SEFM \u201905","author":"Jacobs B.","year":"2005","unstructured":"B. Jacobs, K.R.M. Leino, F. Piessens, and W. Schulte. 2005. Safe concurrency for aggregate objects with invariants. In SEFM \u201905. IEEE, 137\u2013146."},{"key":"e_1_3_2_32_2","first-page":"491","volume-title":"ECOOP \u201904","author":"Leino K. Rustan M.","year":"2004","unstructured":"K. Rustan M. Leino and Peter M\u00fcller. 2004. Object invariants in dynamic contexts. In ECOOP \u201904, Martin Odersky (Ed.). Springer, 491\u2013515."},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/11526841_4","volume-title":"FM 2005: Formal Methods","author":"Leino K. Rustan M.","year":"2005","unstructured":"K. Rustan M. Leino and Peter M\u00fcller. 2005. Modular verification of static class invariants. In FM 2005: Formal Methods, John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki (Eds.). Springer, 26\u201342."},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/1342211.1342225","volume-title":"ISEC \u201908","author":"Leino K. Rustan M.","year":"2008","unstructured":"K. Rustan M. Leino and Angela Wallenburg. 2008. Class-local object invariants. In ISEC \u201908. ACM Press, 57."},{"key":"e_1_3_2_35_2","first-page":"202","volume-title":"ECOOP \u201907","author":"Lu Yi","year":"2007","unstructured":"Yi Lu, John Potter, and Jingling Xue. 2007. Validity invariants and effects. In ECOOP \u201907, Erik Ernst (Ed.), Vol. 4609. Springer, 202\u2013226."},{"issue":"2","key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1002\/stvr.327","article-title":"Exploiting design patterns to automate validation of class invariants","volume":"16","author":"Malloy Brian A.","year":"2006","unstructured":"Brian A. Malloy and James F. Power. 2006. Exploiting design patterns to automate validation of class invariants. Softw. Test. Verif. Reliabil. 16, 2 (Jun.2006), 71\u201395.","journal-title":"Softw. Test. Verif. Reliabil."},{"key":"e_1_3_2_37_2","unstructured":"Marx Brothers. 1935. A Night at the Opera. https:\/\/youtu.be\/G_Sy6oiJbEk?t=228. (1935)."},{"key":"e_1_3_2_38_2","volume-title":"Eiffel: A Language for Software Engineering","author":"Meyer Bertrand","year":"1985","unstructured":"Bertrand Meyer. 1985. Eiffel: A Language for Software Engineering. Technical Report TR-CS-85-19. University of California, Santa Barbara."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(88)90022-2"},{"key":"e_1_3_2_40_2","volume-title":"Object-oriented Software Construction (1st ed.)","author":"Meyer Bertrand","year":"1988","unstructured":"Bertrand Meyer. 1988. Object-oriented Software Construction (1st ed.). Prentice-Hall."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/1-4020-3532-2_4","volume-title":"Engineering Theories of Software Intensive Systems","author":"Meyer Bertrand","year":"2005","unstructured":"Bertrand Meyer. 2005. The dependent delegate dilemma. In Engineering Theories of Software Intensive Systems, Manfred Broy, Johannes Gr\u00fcnbauer, David Harel, and Tony Hoare (Eds.), Vol. 195. Springer, 105\u2013118."},{"key":"e_1_3_2_43_2","unstructured":"Bertrand Meyer. 2021. Class invariants: Concepts problems solutions. arXiv: 1608.07637. Retrieved from https:\/\/arxiv.org\/abs\/1608.07637"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.025"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.08.034"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/1767748"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/11561163_11"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.035"},{"key":"e_1_3_2_50_2","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/567067.567073","volume-title":"POPL \u201983","author":"Nelson Greg","year":"1983","unstructured":"Greg Nelson. 1983. Verifying reachability invariants of linked structures. In POPL \u201983. ACM Press, 38\u201347."},{"issue":"12","key":"e_1_3_2_51_2","doi-asserted-by":"crossref","first-page":"1053","DOI":"10.1145\/361598.361623","article-title":"On the criteria to be used in decomposing systems into modules","volume":"16","author":"Parnas David L.","year":"1972","unstructured":"David L. Parnas. 1972. On the criteria to be used in decomposing systems into modules. Commun. ACM 16, 12 (Dec.1972), 1053\u20131058.","journal-title":"Commun. ACM"},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1007\/978-3-319-06410-9_35","volume-title":"FM 2014: Formal Methods","author":"Polikarpova Nadia","year":"2014","unstructured":"Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer. 2014. Flexible invariants through semantic collaboration. In FM 2014: Formal Methods, Cliff Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Springer, 514\u2013530."},{"key":"e_1_3_2_53_2","first-page":"55","volume-title":"LICS \u201902","author":"Reynolds J. C.","year":"2002","unstructured":"J. C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS \u201902. IEEE, 55\u201374."},{"key":"e_1_3_2_54_2","unstructured":"Emin G\u00fcn Sirer. 2016. Reentrancy Woes in Smart Contracts. Retrieved from https:\/\/hackingdistributed.com\/2016\/07\/13\/reentrancy-woes\/"},{"key":"e_1_3_2_55_2","first-page":"36","volume-title":"TOOLS-Pacific \u201900","author":"Skevoulis S.","year":"2000","unstructured":"S. Skevoulis and Xiaoping Jia. 2000. Generic invariant-based static analysis tool for detection of runtime errors in Java programs. In TOOLS-Pacific \u201900. IEEE, 36\u201344."},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"Tillmann Nikolai","year":"2008","unstructured":"Nikolai Tillmann and Jonathan de Halleux. 2008. Pex\u2013white box test generation for .NET. In Tests and Proofs, Bernhard Beckert and Reiner H\u00e4hnle (Eds.). Springer, 134\u2013153."},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081749"},{"key":"e_1_3_2_58_2","volume-title":"The Object Constraint Language: Getting your Models Ready for MDA (2nd ed.)","author":"Warmer Jos B.","year":"2003","unstructured":"Jos B. Warmer and Anneke G. Kleppe. 2003. The Object Constraint Language: Getting your Models Ready for MDA (2nd ed.). Addison-Wesley."},{"key":"e_1_3_2_59_2","unstructured":"Wikipedia. Accounting Equation. Retrieved from https:\/\/en.wikipedia.org\/wiki\/Accounting_equation"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233830"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626201","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3626201","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:17Z","timestamp":1750178177000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626201"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,20]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3,31]]}},"alternative-id":["10.1145\/3626201"],"URL":"https:\/\/doi.org\/10.1145\/3626201","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,20]]},"assertion":[{"value":"2021-12-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-23","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}