Specifying linked data structures in JML for combining formal verification and testing
The work
| Authors | Christoph Gladisch; Shmuel Tyszberowicz |
|---|---|
| Editors | |
| Type | article |
| Year | 2015 |
| Citekey | gladisch2015specifying |
Where it appeared
| Published in | Science of Computer Programming |
|---|---|
| Publisher | Elsevier BV |
| Volume | 107-108 |
| Pages | 19--40 |
Identifiers
| DOI | 10.1016/j.scico.2015.02.005 |
|---|---|
| OpenAlex | W1981467734 |
| ISSN | 0167-6423 |
Access
| Landing page | https://doi.org/10.1016/j.scico.2015.02.005 |
|---|---|
| Free full text | https://www.sciencedirect.com/science/article/pii/S0167642315000398/pdf |
Empty on purpose
| copy |
Abstract
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.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{gladisch2015specifying,
title = {Specifying linked data structures in JML for combining formal verification and testing},
author = {Christoph Gladisch and Shmuel Tyszberowicz},
year = {2015},
journal = {Science of Computer Programming},
publisher = {Elsevier BV},
volume = {107-108},
pages = {19--40},
issn = {0167-6423},
doi = {10.1016/j.scico.2015.02.005},
}
This record lives at https://refs.drheap.org/gladisch2015specifying/ and will keep doing so.