2026-07-25T16:23:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9230 2024-03-06T10:43:40Z ddc:004 open_access

Definite Reference Mutability Milanova, Ana reference immutability type inference CFL-reachability precision Reference immutability type systems such as Javari and ReIm ensure that a given reference cannot be used to mutate the referenced object. These systems are conservative in the sense that a mutable reference may be mutable due to approximation. In this paper, we present ReM (for definite Re[ference] M[utability]). It separates mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. In addition, we propose a CFL-reachability system for reference immutability, and prove that it is equivalent to ReIm/ReM, thus building a novel framework for reasoning about correctness of reference immutability type systems. We have implemented ReM and applied it on a large benchmark suite. Our results show that approximately 86.5% of all mutable references are definitely mutable. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ana Milanova 2018 Is Part Of LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2018.25 urn:nbn:de:0030-drops-92303 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.25 eng https://creativecommons.org/licenses/by/3.0/legalcode