Towards Categorizing and Formalizing the JDK API

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

Permalink

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

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

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

Language

en

Permalink

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

Owning Collections