Digital Commons Network^™

Writing Jml Specifications Using Java 8 Streams, Yoonsik Cheon, Zejing Cao, Khandoker Rahad

Departmental Technical Reports (CS)

JML is a formal behavioral interface specification language for Java to document Java program modules such as classes and interfaces. When composing JML specifications, one frequently writes assertions involving a collection of values. In this paper we propose to use Java 8 streams for writing more concise and cleaner assertions on a collection. The use of streams in JML can be minimal and non-invasive in the conventional style of writing assertions. It can also be holistic to write all assertions in the abstract state defined by streams. We perform a small case study to illustrate our approach and show its …