Utilize este identificador para referenciar este registo: http://hdl.handle.net/10362/180306
Registo completo
Campo DCValorIdioma
dc.contributor.authorBacchiani, Lorenzo-
dc.contributor.authorBravetti, Mario-
dc.contributor.authorGiunti, Marco-
dc.contributor.authorMota, João-
dc.contributor.authorRavara, António-
dc.date.accessioned2025-03-08T00:23:19Z-
dc.date.available2025-03-08T00:23:19Z-
dc.date.issued2024-09-
dc.identifier.isbn9783959773416-
dc.identifier.issn1868-8969-
dc.identifier.otherPURE: 100945966-
dc.identifier.otherPURE UUID: 34121791-e6eb-48b4-88d7-244124656e30-
dc.identifier.otherScopus: 85205002570-
dc.identifier.otherORCID: /0000-0001-8074-0380/work/179618082-
dc.identifier.urihttp://hdl.handle.net/10362/180306-
dc.descriptionPublisher Copyright: © Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara;-
dc.description.abstractWe 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.isoeng-
dc.publisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing-
dc.relationinfo:eu-repo/grantAgreement/EC/H2020/778233/EU-
dc.rightsopenAccess-
dc.subjectBehavioural types-
dc.subjectcast-
dc.subjectobject-oriented programming-
dc.subjectsubtyping-
dc.subjecttypestates-
dc.subjectSoftware-
dc.titleBehavioural Up/down Casting For Statically Typed Languages-
dc.typeconferenceObject-
degois.publication.title38th European Conference on Object-Oriented Programming, ECOOP 2024-
degois.publication.title38th European Conference on Object-Oriented Programming, ECOOP 2024-
degois.publication.volume313-
dc.peerreviewedyes-
dc.identifier.doihttps://doi.org/10.4230/LIPIcs.ECOOP.2024.5-
dc.description.versionpublishersversion-
dc.description.versionpublished-
dc.contributor.institutionFaculdade de Ciências e Tecnologia (FCT)-
dc.contributor.institutionNOVALincs-
Aparece nas colecções:Home collection (FCT)

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
LIPIcs.ECOOP.2024.5.pdf1,26 MBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.