{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:48:20Z","timestamp":1756000100796,"version":"3.40.4"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Traits have been proposed as a more flexible mechanism than class inheritance for structuring code in object-oriented programming, to achieve fine-grained code reuse. A trait originally developed for one purpose can be adapted and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. So far, work on formally establishing properties of trait-based programs has mostly concentrated on type systems. This paper presents the first deductive proof system for a trait-based object-oriented language. If a specification of a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. However, imposing such a restriction may in many cases unnecessarily limit traits as a mechanism for flexible code reuse. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in an<jats:italic>incremental<\/jats:italic>way which does not violate established proofs. We formalize and show the soundness of the proof system.<\/jats:p>","DOI":"10.1007\/s00165-013-0278-3","type":"journal-article","created":{"date-parts":[[2013,5,16]],"date-time":"2013-05-16T11:46:21Z","timestamp":1368704781000},"page":"761-793","source":"Crossref","is-referenced-by-count":9,"title":["Verifying traits: an incremental proof system for fine-grained reuse"],"prefix":"10.1145","volume":"26","author":[{"given":"Ferruccio","family":"Damiani","sequence":"first","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Torino, Torino, Italy"}]},{"given":"Johan","family":"Dovland","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Oslo, PO Box 1080, 0316, Blindern, Oslo, Norway"}]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Oslo, PO Box 1080, 0316, Blindern, Oslo, Norway"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"Institute for Software Engineering, Technische Universit\u00e4t Braunschweig, Brunswick, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Apt KR de Boer FS Olderog ER (2009) Verification of sequential and concurrent systems. Texts and Monographs in Computer Science 3rd edn. Springer Berlin","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.120"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aldrich J (2005) Open modules: modular reasoning about advice. In: Black AP (ed) Proceedings of European conference on object-oriented programming (ECOOP) volume 3586 of lecture notes in computer science pp 144\u2013168. Springer Berlin","DOI":"10.1007\/11531142_7"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/937563.937567"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"America P (1991) Designing an object-oriented programming language with behavioural subtyping. In: de Bakker JW de Roever W-P Rozenberg G (eds) Foundations of object-oriented languages volume 489 of lecture notes in computer science pp 60\u201390. Springer Berlin","DOI":"10.1007\/BFb0019440"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bracha G Cook W (1990) Mixin-based inheritance. In: Meyrowitz N (ed) Proceedings of the conference on object-oriented programming: systems languages and applications \/ European conference on object-oriented programming pp 303\u2013311. ACM Press New York","DOI":"10.1145\/97945.97982"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bettini L Capecchi S Damiani F (2012) On flexible dynamic trait repacement for Java-like languages. Sci Comput Program. Available online doi:10.1016\/j.scico.2012.11.003","DOI":"10.1016\/j.scico.2012.11.003"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bettini L Damiani F De Luca M Geilmann K Sch\u00e4fer J (2010) A calculus for boxes and traits in a Java-like setting. In: Clarke D Agha G (eds) Coordination models and languages volume 6116 of lecture notes in computer science pp 46\u201360. Springer Berlin","DOI":"10.1007\/978-3-642-13414-2_4"},{"key":"e_1_2_1_2_11_2","unstructured":"Bono V Damiani F Giachino E (2007) Separating type behavior and state to achieve very fine-grained reuse. In: Proceedings of formal techniques for Java-like Programs (FTfJP)"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bono V Damiani F Giachino E (2008) On traits and types in a Java-like setting. In: Fifth IFIP international conference on theoretical computer science (TCS\u201908) volume 273 of international federation for information processing pp 367\u2013382. Springer Berlin","DOI":"10.1007\/978-0-387-09680-3_25"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.10.006"},{"key":"e_1_2_1_2_14_2","unstructured":"Black A Ducasse S Nierstrasz O Pollet D Cassou D Denker M (2009) Pharo by example. Square Bracket Associates"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2007.05.003"},{"key":"e_1_2_1_2_16_2","unstructured":"Bettini L Damiani F Schaefer I (2009) Implementing SPL using Traits. Technical report Dipartimento di Informatica Universit\u00e0 di Torino. Available at http:\/\/www.di.unito.it\/~damiani\/papers\/isplurat.pdf"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Bettini L Damiani F Schaefer I (2010) Implementing software product lines using traits. In: Proceedings of the 2010 ACM symposium on applied computing (SAC\u201910) pp 2096\u20132102. ACM Press New York","DOI":"10.1145\/1774088.1774530"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Bettini L Damiani F Schaefer I Strocco F (2010) A prototypical Java-like language with records and traits. In: Proceedings of the 8th international conference on the principles and practice of programming in Java (PPPJ\u201910) pp 129\u2013138. ACM Press New York","DOI":"10.1145\/1852761.1852780"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.06.007"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Beckert B H\u00e4hnle R Schmitt PH (eds) (2007) Verification of object-oriented software: the key approach volume 4334 of lecture notes in computer science. Springer Berlin","DOI":"10.1007\/978-3-540-69061-0"},{"key":"e_1_2_1_2_21_2","unstructured":"Booch G Rumbaugh JE Jacobson I (1999) The unified modeling language user guide. Addison-Wesley Reading"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Bagherzadeh M Rajan H Leavens GT Mooney SL (2011) Translucid contracts: expressive specification and modular verification for aspect-oriented interfaces. In: Borba P Chiba S (eds) Proceedings of the 10th international conference on aspect-oriented software development (AOSD 2011) pp 141\u2013152. ACM Press New York","DOI":"10.1145\/1960275.1960293"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.23"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Back R-J von Wright J (1998) Refinement calculus: a systematic introduction. Graduate texts in computer science. Springer Berlin","DOI":"10.1007\/978-1-4612-1674-2_1"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"de Boer FS (1999) A WP-calculus for OO. In: Thomas W (ed) Proceedings of foundations of software science and computation structure (FOSSACS\u201999) volume 1578 of lecture notes in computer science pp 135\u2013149. Springer Berlin","DOI":"10.1007\/3-540-49019-1_10"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Damiani F Dovland J Johnsen EB Owe O Schaefer I Yu IC (2012) A transformational proof system for delta-oriented programming. In: de Almeida ES Schwanninger C Benavides D (eds) Proceedings of 16th international software product line conference (SPLC\u201912) vol 2 pp 53\u201360. ACM Press New York","DOI":"10.1145\/2364412.2364422"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Damiani F Dovland J Johnsen EB Schaefer I (2011) Verifying traits: a proof system for fine-grained reuse. In: Proceedings of formal techniques for Java-like programs (FTfJP) pp 8:1\u20138:6. ACM Press New York","DOI":"10.1145\/2076674.2076682"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.07.008"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.09.006"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1119479.1119483"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"De Fraine B Ernst E S\u00fcdholt M (2010) Essential AOP: the A calculus. In: D\u2019Hondt T (ed) Proceedings of European conference on object-oriented programming (ECOOP) volume 6183 of lecture notes in computer science pp 101\u2013125. Springer Berlin","DOI":"10.1007\/978-3-642-14107-2_6"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Flatt M Krishnamurthi S Felleisen M (1998) Classes and mixins. In: Proceedings of principles of programming languages (POPL) pp 171\u2013183. ACM Press New York","DOI":"10.1145\/268946.268961"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1971) Procedures and parameters: An axiomatic approach. In: Engeler E (e) Symposium on semantics of algorithmic languages volume 188 of lecture notes in mathematics pp 102\u2013116. Springer Berlin","DOI":"10.1007\/BFb0059696"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle R Schaefer I (2012) A Liskov principle for delta-oriented programming. In: Margaria T Steffen B (eds) Proceedings of 5th international symposium on leveraging applications of formal methods verification and validation (ISoLA) volume 7609 of lecture notes in computer science pp 32\u201346. Springer Berlin","DOI":"10.1007\/978-3-642-34026-0_4"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.031"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Krishnamurthi S Fisler K (2007) Foundations of incremental aspect model-checking. Trans Softw Eng Methodol 16(2)","DOI":"10.1145\/1217295.1217296"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Kiczales G Lamping J Mendhekar A Maeda C Lopes C Loingtier J-M Irwin J (1997) Aspect-oriented programming. In: Ak\u015fit M Matsuoka S (eds) Proceedings of European conference on object-oriented programming (ECOOP) volume 1241 of lecture notes in computer science pp 220\u2013242. Springer Berlin","DOI":"10.1007\/BFb0053381"},{"key":"e_1_2_1_2_41_2","unstructured":"Leavens GT Naumann DA (2006) Behavioral subtyping specification inheritance and modular reasoning. Technical Report 06-20a Department of Computer Science Iowa State University Ames"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Luo C Qin S (2008) Separation logic for multiple inheritance. Electronic Notes in Theoretical Computer Science. In: Proceedings of first international conference on foundations of informatics computing and software (FICS) vol 212 pp 27\u201340","DOI":"10.1016\/j.entcs.2008.04.051"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.051"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/1330017.1330022"},{"key":"e_1_2_1_2_45_2","unstructured":"Lagorio G Servetto M Zucca E (2009) Flattening versus direct semantics for featherweight jigsaw. In: Proceedings of workshop on foundations of object-oriented languages (FOOL)"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"#cr-split#-e_1_2_1_2_47_2.1","doi-asserted-by":"crossref","unstructured":"Nordio M Calcagno C M\u00fcller P Meyer B (2009) A sound and complete program logic for eiffel. In: Oriol M","DOI":"10.1007\/978-3-642-02571-6_12"},{"key":"#cr-split#-e_1_2_1_2_47_2.2","unstructured":"(ed) TOOLS-EUROPE 2009 volume 33 of lecture notes in business and information processing pp 195-214"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2006.5.4.a4"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_2_50_2","unstructured":"Odersky M Spoon L Venners B (2010) Programming in Scala 2 edn. Artima Press California"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Parkinson MJ Bierman GM (2008) Separation logic abstraction and inheritance. In: Proceedings of principles of programming languages (POPL) pp 75\u201386. ACM Press New York","DOI":"10.1145\/1328897.1328451"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Parkinson MJ Bornat R Calcagno C (2006) Variables as resource in Hoare logics. In: Proceedings of symposium on logic in computer science (LICS\u201906) pp 137\u2013146. IEEE Computer Society Press New York","DOI":"10.1109\/LICS.2006.52"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Poetzsch-Heffter A M\u00fcller P (1999) A programming logic for sequential Java. In: Swierstra SD (ed) 8th European symposium on programming languages and systems (ESOP\u201999) volume 1576 of lecture notes in computer science pp 162\u2013176. Springer Berlin","DOI":"10.1007\/3-540-49099-X_11"},{"key":"e_1_2_1_2_54_2","unstructured":"Reppy JH Turon A (2006) A foundation for trait-based metaprogramming. In: Proceedings of FOOL\/WOOD"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Reppy JH Turon A (2007) Metaprogramming with traits. In: Proceedings of European conference on object-oriented programming (ECOOP) volume 4609 of lecture notes in computer science pp 373\u2013398. Springer Berlin","DOI":"10.1007\/978-3-540-73589-2_18"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Steele Jr GL Allen EE Chase D Flood CH Luchangco V Maessen J-W Ryu S (2011) Fortress (Sun HPCS language). In: Padua DA (ed) Encyclopedia of parallel computing pp 718\u2013735. Springer Berlin","DOI":"10.1007\/978-0-387-09766-4_190"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Schaefer I Bettini L Bono V Damiani F Tanzarella N (2010) Delta-oriented programming of software product lines. In: Bosch J Lee J (eds) Software product lines: going beyond (SPLC\u201910) volume 6287 of lecture notes in computer science pp 77\u201391. Springer Berlin","DOI":"10.1007\/978-3-642-15579-6_6"},{"key":"e_1_2_1_2_58_2","unstructured":"Schwerhoff M (2010) Verifying scala traits. Semester Report Swiss Federal Institute of Technology Zurich (ETH)"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Smith C Drossopoulou S (2005) Chai : traits for Java-like languages. In: Proceedings of European conference on object-oriented programming (ECOOP) volume 3586 of lecture notes in computer science pp 453\u2013478. Springer Berlin","DOI":"10.1007\/11531142_20"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Sch\u00e4rli N Ducasse S Nierstrasz O Black A (2003) Traits: composable units of behavior. In: Proceedings of European conference on object-oriented programming (ECOOP) volume 2743 of lecture notes in computer science pp 248\u2013274. Springer Berlin","DOI":"10.1007\/978-3-540-45070-2_12"},{"key":"e_1_2_1_2_61_2","unstructured":"TraitRecordJ website (2011) http:\/\/traitrecordj.sourceforge.net\/"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Th\u00fcm T Schaefer I Apel S Hentschel M (2012) Family-based deductive verification of software product lines. In: International conference on generative programming and component engineering (GPCE) pp 11\u201320. ACM Press New York","DOI":"10.1145\/2371401.2371404"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"crossref","unstructured":"Th\u00fcm T Schaefer I Kuhlemann M Apel S (2011) Proof composition for deductive verification of software product lines. In: Proceedings of international workshop on variability-intensive systems testing validation and verification pp 270\u2013277. IEEE Computer Society Press New York","DOI":"10.1109\/ICSTW.2011.48"},{"issue":"1","key":"e_1_2_1_2_64_2","first-page":"1","article-title":"Encapsulation and composition as orthogonal operators on mixins: A solution to multiple inheritance problems","volume":"3","author":"Van Limberghen M","year":"1996","journal-title":"Object Oriented Syst"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"crossref","unstructured":"van Staden S Calcagno C (2010) Reasoning about multiple related abstractions with MultiStar. In: Proceedings of object-oriented programming systems languages and applications (OOPSLA) pp 504\u2013519. ACM Press New York","DOI":"10.1145\/1932682.1869501"},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"crossref","unstructured":"Wills A (1991) Capsules and types in fresco: program verification in smalltalk. In: America P (ed) Proceedings of European conference on object-oriented programming (ECOOP) volume 512 of lecture notes in computer science pp 59\u201376. Springer Berlin","DOI":"10.1007\/BFb0057015"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0278-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0278-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0278-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T10:22:07Z","timestamp":1746008527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0278-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":67,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1007\/s00165-013-0278-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0278-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2014,7]]}}}