Formal specification with JML

Marieke Huisman; Wolfgang Ahrendt; Daniel Bruns; Martin Hentschel

Formal specification with JML

Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, Martin Hentschel

Research output: Book/Report › Report › Professional

380 Downloads (Pure)

Abstract

This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.

Original language	English
Place of Publication	Karlsruhe
Publisher	Karlsruhe Institute of Technology
Number of pages	51
Publication status	Published - 2014

Publication series

Name	Karlsruhe Reports in Informatics
Publisher	Karlsruhe Institute of Technology, Department of Informatics
No.	2014-10
ISSN (Print)	2190-4782

Keywords

EC Grant Agreement nr.: FP7/287767
EC Grant Agreement nr.: FP7/258405
EC Grant Agreement nr.: FP7/2007-2013

Access to Document

http://digbib.ubka.uni-karlsruhe.de/volltexte/1000041881

Cite this

@book{56a5e40cbe494172b7692205841a0355,

title = "Formal specification with JML",

abstract = "This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.",

keywords = "EC Grant Agreement nr.: FP7/287767, EC Grant Agreement nr.: FP7/258405, EC Grant Agreement nr.: FP7/2007-2013",

author = "Marieke Huisman and Wolfgang Ahrendt and Daniel Bruns and Martin Hentschel",

note = "eemcs-eprint-25720 ",

year = "2014",

language = "English",

series = "Karlsruhe Reports in Informatics",

publisher = "Karlsruhe Institute of Technology",

number = "2014-10",

}

TY - BOOK

T1 - Formal specification with JML

AU - Huisman, Marieke

AU - Ahrendt, Wolfgang

AU - Bruns, Daniel

AU - Hentschel, Martin

N1 - eemcs-eprint-25720

PY - 2014

Y1 - 2014

N2 - This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.

AB - This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.

KW - EC Grant Agreement nr.: FP7/287767

KW - EC Grant Agreement nr.: FP7/258405

KW - EC Grant Agreement nr.: FP7/2007-2013

M3 - Report

T3 - Karlsruhe Reports in Informatics

BT - Formal specification with JML

PB - Karlsruhe Institute of Technology

CY - Karlsruhe

ER -

Formal specification with JML

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this