Utilize este identificador para referenciar este registo:
http://hdl.handle.net/10362/180306
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Bacchiani, Lorenzo | - |
dc.contributor.author | Bravetti, Mario | - |
dc.contributor.author | Giunti, Marco | - |
dc.contributor.author | Mota, João | - |
dc.contributor.author | Ravara, António | - |
dc.date.accessioned | 2025-03-08T00:23:19Z | - |
dc.date.available | 2025-03-08T00:23:19Z | - |
dc.date.issued | 2024-09 | - |
dc.identifier.isbn | 9783959773416 | - |
dc.identifier.issn | 1868-8969 | - |
dc.identifier.other | PURE: 100945966 | - |
dc.identifier.other | PURE UUID: 34121791-e6eb-48b4-88d7-244124656e30 | - |
dc.identifier.other | Scopus: 85205002570 | - |
dc.identifier.other | ORCID: /0000-0001-8074-0380/work/179618082 | - |
dc.identifier.uri | http://hdl.handle.net/10362/180306 | - |
dc.description | Publisher Copyright: © Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara; | - |
dc.description.abstract | We provide support for polymorphism in static typestate analysis for object-oriented languages with upcasts and downcasts. Recent work has shown how typestate analysis can be embedded in the development of Java programs to obtain safer behaviour at runtime, e.g., absence of null pointer errors and protocol completion. In that approach, inheritance is supported at the price of limiting casts in source code, thus only allowing those at the beginning of the protocol, i.e., immediately after objects creation, or at the end, and in turn seriously affecting the applicability of the analysis. In this paper, we provide a solution to this open problem in typestate analysis by introducing a theory based on a richer data structure, named typestate tree, which supports upcast and downcast operations at any point of the protocol by leveraging union and intersection types. The soundness of the typestate tree-based approach has been mechanised in Coq. The theory can be applied to most object-oriented languages statically analysable through typestates, thus opening new scenarios for acceptance of programs exploiting inheritance and casting. To defend this thesis, we show an application of the theory, by embedding the typestate tree mechanism in a Java-like object-oriented language, and proving its soundness. | en |
dc.language.iso | eng | - |
dc.publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing | - |
dc.relation | info:eu-repo/grantAgreement/EC/H2020/778233/EU | - |
dc.rights | openAccess | - |
dc.subject | Behavioural types | - |
dc.subject | cast | - |
dc.subject | object-oriented programming | - |
dc.subject | subtyping | - |
dc.subject | typestates | - |
dc.subject | Software | - |
dc.title | Behavioural Up/down Casting For Statically Typed Languages | - |
dc.type | conferenceObject | - |
degois.publication.title | 38th European Conference on Object-Oriented Programming, ECOOP 2024 | - |
degois.publication.title | 38th European Conference on Object-Oriented Programming, ECOOP 2024 | - |
degois.publication.volume | 313 | - |
dc.peerreviewed | yes | - |
dc.identifier.doi | https://doi.org/10.4230/LIPIcs.ECOOP.2024.5 | - |
dc.description.version | publishersversion | - |
dc.description.version | published | - |
dc.contributor.institution | Faculdade de Ciências e Tecnologia (FCT) | - |
dc.contributor.institution | NOVALincs | - |
Aparece nas colecções: | Home collection (FCT) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
LIPIcs.ECOOP.2024.5.pdf | 1,26 MB | Adobe PDF | Ver/Abrir |
Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.