Specifying linked data structures in JML for combining formal verification and testing

• We specified in JML and verified operations on linked lists and binary trees.
• Concise and readable specifications of linked data structures are provided.
• The same specifications are used for formal deductive verification and testing.
• Using queries in specification is a verification challenge that we address.
• A set of new verification techniques implemented in the KeY tool is presented.

We show how to write concise and readable specifications of linked data structures that are applicable for both formal deductive verification and testing. A singly linked list and a binary search tree are provided as examples. The main characteristic of the specifications is the use of observer methods, in particular to express reachability of elements in a data structure. The specifications are written in the Java Modeling Language (JML) and do not require extensions of that language. This paper addresses a mixed audience of users and developers in the fields of formal verification, testing, and specification language design. We provide an in-depth description of the proposed specifications and analyze the implications both for verification and testing. Based on this analysis we have developed verification techniques that are implemented in the deductive verification tool KeY and enable fully automatic verification of the linked list example. This techniques are also described in this paper.