IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Towards Categorizing and Formalizing the JDK API

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/30006

Files in this item

File Description Format
PDF lee-jin-meredith-rosu-2012-tr-1.pdf (590KB) (no description provided) PDF
Title: Towards Categorizing and Formalizing the JDK API
Author(s): Lee, Choonghwan; Jin, Dongyun; Meredith, Patrick O'Neil; Rosu, Grigore
Subject(s): Verification debugging
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.
Issue Date: 2012-03-12
Genre: Technical Report
Type: Text
Language: English
URI: http://hdl.handle.net/2142/30006
Publication Status: published or submitted for publication
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2012-03-12
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 128
  • Downloads this Month: 3
  • Downloads Today: 0

Browse

My Account

Information

Access Key