A carregar...
Publicação
A Java typestate checker supporting inheritance
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 274.97 KB | Adobe PDF |
Orientador(es)
Resumo(s)
Detecting programming errors in software is increasingly important, and building tools that help developers with this task is a crucial area of investigation on which the industry depends. Leveraging on the observation that in Object-Oriented Programming (OOP) it is natural to define stateful objects where the safe use of methods depends on their internal state, we present Java Typestate Checker (JATYC), a tool that verifies Java source code with respect to typestates. A typestate defines the object's states, the methods that can be called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey to object's protocols; objects' protocols are completed; null-pointer exceptions are not raised; subclasses' instances respect the protocol of their superclasses. To the best of our knowledge, this is the first OOP tool that simultaneously tackles all these aspects.
Descrição
This work was partially supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No. 778233 (BehAPI) and by NOVA LINCS UIDB/04516/2020/TRA/BIM/07 ) via the Portuguese Fundação para a Ciência e a Tecnologia.
Publisher Copyright:
© 2022 Elsevier B.V.
Palavras-chave
Behavioral types Object-oriented programming Subtyping Type-checking Typestates Software Computational Theory and Mathematics General Computer Science SDG 9 - Industry, Innovation, and Infrastructure