View in EDS

A Java typestate checker supporting inheritance.

Saved in:

Bibliographic Details
Title:	A Java typestate checker supporting inheritance.
Authors:	Bacchiani, Lorenzo¹ (AUTHOR), Bravetti, Mario^1,2 (AUTHOR), Giunti, Marco³ (AUTHOR), Mota, João^1,3 (AUTHOR) jd.mota@campus.fct.unl.pt, Ravara, António³ (AUTHOR)
Source:	Science of Computer Programming. Sep2022, Vol. 221, pN.PAG-N.PAG. 1p.
Subjects:	Object-oriented programming, Source code
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. • Java Typestate Checker is a tool that verifies Java code with respect to typestates. • It verifies that sequences of method calls obey to object's protocols. • It verifies that objects' protocols are completed. • It verifies that null-pointer exceptions are not raised. • It verifies that subclasses' instances respect the protocol of their superclasses. [ABSTRACT FROM AUTHOR]
	Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
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. • Java Typestate Checker is a tool that verifies Java code with respect to typestates. • It verifies that sequences of method calls obey to object's protocols. • It verifies that objects' protocols are completed. • It verifies that null-pointer exceptions are not raised. • It verifies that subclasses' instances respect the protocol of their superclasses. [ABSTRACT FROM AUTHOR]
ISSN:	01676423
DOI:	10.1016/j.scico.2022.102844