Formal specication 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 specications 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 specication. This paper presents a tool-supported approach to help writing formal specications for Java libraries and creating documentation augmented with highlighting and formal specications. 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 specications. Indirectly, this paper also brings empirical evidence that parametric specications may be suciently powerful to express virtually all desirable runtime properties of the JDK API, and that its informal documentation can be formalized.
分享
引用
