Java Typestate Checker - Coordination Models and Languages Access content directly
Conference Papers Year : 2021

Java Typestate Checker

Abstract

Detecting programming errors and vulnerabilities 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. In object-oriented languages, one naturally defines stateful objects where the safe use of methods depends on their internal state; the correct use of objects according to their protocols is then enforced at compile-time by an analysis based on behavioral types.We present Java Typestate Checker (JATYC), a tool based on the Checker Framework that verifies Java programs with respect to typestates. These define the object’s states, the methods that can be called in each state, and the states resulting from the calls. The tool offers the following strong guarantees: sequences of method calls obey to object’s protocols; completion of objects’ protocols; detection of null-pointer exceptions; and control of the sharing of resources through access permissions.To the best of our knowledge, there are no research or industrial tools that offer all these features. In particular, the implementation of sharing control in a typestate-based tool seems to be novel, and has an important impact on programming flexibility, since, for most programs, the linear discipline imposed by behavioral types is too strict.Sharing of objects is enabled by means of an assertion language incorporating fractional permissions; to lift from programmers the burden of writing the assertions, JATYC infers all of these by building a constraint system and solving it with Z3, producing general assertions sufficient to accept the code, if these exist.
Fichier principal
Vignette du fichier
509400_1_En_8_Chapter.pdf (333.56 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03387832 , version 1 (20-10-2021)

Licence

Attribution

Identifiers

Cite

João Mota, Marco Giunti, António Ravara. Java Typestate Checker. 23th International Conference on Coordination Languages and Models (COORDINATION), Jun 2021, Valletta, Malta. pp.121-133, ⟨10.1007/978-3-030-78142-2_8⟩. ⟨hal-03387832⟩
57 View
29 Download

Altmetric

Share

Gmail Facebook X LinkedIn More