University of Illinois Urbana-Champaign

Towards Categorizing and Formalizing the JDK API

Lee, Choonghwan; Jin, Dongyun; Meredith, Patrick O'Neil; Rosu, Grigore

Content Files
lee-jin-meredith-rosu-2012-tr-1.pdf

Permalink

https://hdl.handle.net/2142/30006

Description

Title
Towards Categorizing and Formalizing the JDK API
Author(s)
  • Lee, Choonghwan
  • Jin, Dongyun
  • Meredith, Patrick O'Neil
  • Rosu, Grigore
Issue Date
2012-03-12
Keyword(s)
  • Verification
  • debugging
Date of Ingest
2012-03-12T18:26:52Z
Abstract
Formal specification of correct library usage is extremely useful, both for software developers and for the formal analysis tools they use, such as model checkers or runtime monitoring systems. Unfortunately, the process of creating formal specifications is time consuming, and, for the most part, even the libraries in greatest use, such as the Java Development Kit (JDK) standard library, are left wholly without formal specification. This paper presents a tool-supported approach to help writing formal specifications for Java libraries and creating documentation augmented with highlighting and formal specifications. The presented approach has been applied to systematically and completely formalize the runtime properties of three core and commonly used packages of the JDK API, namely java.io, java.lang and java.util, yielding 137 formal specifications. Indirectly, this paper also brings empirical evidence that parametric specifications may be sufficiently powerful to express virtually all desirable runtime properties of the JDK API, and that its informal documentation can be formalized.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/30006

Owning Collections

Research and Tech Reports - Computer Science PRIMARY