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.
| Original language | English |
|---|---|
| Title of host publication | FTfJP 2021 - Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, co-located with ECOOP/ISSTA 2021 |
| Editors | David R. Cok |
| Number of pages | 8 |
| Publisher | Association for Computing Machinery |
| Publication date | 13 Jul 2021 |
| Pages | 51-58 |
| ISBN (Electronic) | 978-1-4503-8543-5 |
| DOIs | |
| Publication status | Published - 13 Jul 2021 |
| Event | 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021 - Virtual, Online, Denmark Duration: 13 Jul 2021 → 13 Jul 2021 |
Conference
| Conference | 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021 |
|---|---|
| Country/Territory | Denmark |
| City | Virtual, Online |
| Period | 13/07/2021 → 13/07/2021 |
| Sponsor | ACM SIGPLAN |
Bibliographical note
Publisher Copyright:© 2021 ACM.
Keywords
- Behavioural types
- separation logic