Abstract
Mungo is an object-oriented language that uses typestates with a behavioural type system to ensure the absence of null-dereferencing. Typestates are usages that specify the admissible sequences of method calls on objects. Previous type systems for Mungo have all had a linearity constraint on objects. We present an extension of these systems, where usage specifications can now include a parallel construct that lets us describe separate local behaviour. A parallel usage describes a separation of the heap, and this allows us to reason about aliasing and to express arbitrary interleaving of local protocols. This also solves the state-space explosion problem for usages. Our extension retains the safety properties of previous type systems for Mungo.
Originalsprog | Engelsk |
---|---|
Titel | FTfJP 2021 - Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, co-located with ECOOP/ISSTA 2021 |
Redaktører | David R. Cok |
Antal sider | 8 |
Forlag | Association for Computing Machinery |
Publikationsdato | 13 jul. 2021 |
Sider | 51-58 |
ISBN (Elektronisk) | 978-1-4503-8543-5 |
DOI | |
Status | Udgivet - 13 jul. 2021 |
Begivenhed | 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021 - Virtual, Online, Danmark Varighed: 13 jul. 2021 → 13 jul. 2021 |
Konference
Konference | 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021 |
---|---|
Land/Område | Danmark |
By | Virtual, Online |
Periode | 13/07/2021 → 13/07/2021 |
Sponsor | ACM SIGPLAN |
Bibliografisk note
Publisher Copyright:© 2021 ACM.