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.
A Java typestate checker supporting inheritance / Bacchiani L.; Bravetti M.; Giunti M.; Mota J.; Ravara A.. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - ELETTRONICO. - 221:(2022), pp. 102844.1-102844.8. [10.1016/j.scico.2022.102844]
A Java typestate checker supporting inheritance
Bacchiani L.;Bravetti M.;
2022
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
1-s2.0-S0167642322000776-main.pdf
accesso aperto
Tipo:
Versione (PDF) editoriale
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione
274.97 kB
Formato
Adobe PDF
|
274.97 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.