A Java typestate checker supporting inheritance.

Saved in:
Bibliographic Details
Title: A Java typestate checker supporting inheritance.
Authors: Bacchiani, Lorenzo1 (AUTHOR), Bravetti, Mario1,2 (AUTHOR), Giunti, Marco3 (AUTHOR), Mota, João1,3 (AUTHOR) jd.mota@campus.fct.unl.pt, Ravara, António3 (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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 158331448
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: A Java typestate checker supporting inheritance.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Bacchiani%2C+Lorenzo%22">Bacchiani, Lorenzo</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Bravetti%2C+Mario%22">Bravetti, Mario</searchLink><relatesTo>1,2</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Giunti%2C+Marco%22">Giunti, Marco</searchLink><relatesTo>3</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Mota%2C+João%22">Mota, João</searchLink><relatesTo>1,3</relatesTo> (AUTHOR)<i> jd.mota@campus.fct.unl.pt</i><br /><searchLink fieldCode="AR" term="%22Ravara%2C+António%22">Ravara, António</searchLink><relatesTo>3</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Science+of+Computer+Programming%22">Science of Computer Programming</searchLink>. Sep2022, Vol. 221, pN.PAG-N.PAG. 1p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Object-oriented+programming%22">Object-oriented programming</searchLink><br /><searchLink fieldCode="DE" term="%22Source+code%22">Source code</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=158331448
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.scico.2022.102844
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 1
        StartPage: N.PAG
    Subjects:
      – SubjectFull: Object-oriented programming
        Type: general
      – SubjectFull: Source code
        Type: general
    Titles:
      – TitleFull: A Java typestate checker supporting inheritance.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Bacchiani, Lorenzo
      – PersonEntity:
          Name:
            NameFull: Bravetti, Mario
      – PersonEntity:
          Name:
            NameFull: Giunti, Marco
      – PersonEntity:
          Name:
            NameFull: Mota, João
      – PersonEntity:
          Name:
            NameFull: Ravara, António
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 09
              Text: Sep2022
              Type: published
              Y: 2022
          Identifiers:
            – Type: issn-print
              Value: 01676423
          Numbering:
            – Type: volume
              Value: 221
          Titles:
            – TitleFull: Science of Computer Programming
              Type: main
ResultId 1