Prototyping a tool environment for run-time assertion checking in JML with communication histories

Frank S. de Boer; Stijn de Gouw; Jurgen J. Vinju

doi:10.1145/1924520.1924526

Prototyping a tool environment for run-time assertion checking in JML with communication histories

Frank S. de Boer
, Stijn de Gouw
, Jurgen J. Vinju

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

In this paper we present prototype tool-support for the runtime assertion checking of the Java Modeling Language (JML) extended with communication histories specified by attribute grammars. Our tool suite integrates Rascal, a meta programming language and ANTLR, a popular parser generator. Rascal instantiates a generic model of history updates for a given Java program annotated with history specifications. ANTLR is used for the actual evaluation of history assertions.

Original language	English
Title of host publication	Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, Maribor, Slovenia, June 22, 2010
Place of Publication	New York, NY
Publisher	ACM Digital Library
Pages	6:1-6:7
ISBN (Print)	978-1-4503-0540-2
DOIs	https://doi.org/10.1145/1924520.1924526
Publication status	Published - 2010
Externally published	Yes
Event	12th Workshop on Formal Techniques for Java-like Programs - Maribor, Slovenia Duration: 22 Jun 2010 → 22 Jun 2010 https://distrinet.cs.kuleuven.be/events/ftfjp10/

Workshop

Workshop	12th Workshop on Formal Techniques for Java-like Programs
Abbreviated title	FTfJP 2010
Country/Territory	Slovenia
City	Maribor
Period	22/06/10 → 22/06/10
Internet address	https://distrinet.cs.kuleuven.be/events/ftfjp10/

Access to Document

10.1145/1924520.1924526

Cite this

@inproceedings{e0f3db9d65874db49f1b2a1dab255bb8,

title = "Prototyping a tool environment for run-time assertion checking in JML with communication histories",

abstract = "In this paper we present prototype tool-support for the runtime assertion checking of the Java Modeling Language (JML) extended with communication histories specified by attribute grammars. Our tool suite integrates Rascal, a meta programming language and ANTLR, a popular parser generator. Rascal instantiates a generic model of history updates for a given Java program annotated with history specifications. ANTLR is used for the actual evaluation of history assertions.",

author = "Boer, \{Frank S. de\} and Gouw, \{Stijn de\} and Vinju, \{Jurgen J.\}",

year = "2010",

doi = "10.1145/1924520.1924526",

language = "English",

isbn = "978-1-4503-0540-2 ",

pages = "6:1--6:7",

booktitle = "Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, Maribor, Slovenia, June 22, 2010",

publisher = "ACM Digital Library",

note = "12th Workshop on Formal Techniques for Java-like Programs , FTfJP 2010 ; Conference date: 22-06-2010 Through 22-06-2010",

url = "https://distrinet.cs.kuleuven.be/events/ftfjp10/",

}

Boer, FSD, Gouw, SD & Vinju, JJ 2010, Prototyping a tool environment for run-time assertion checking in JML with communication histories. in Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, Maribor, Slovenia, June 22, 2010., 6, ACM Digital Library, New York, NY, pp. 6:1-6:7, 12th Workshop on Formal Techniques for Java-like Programs , Maribor, Slovenia, 22/06/10. https://doi.org/10.1145/1924520.1924526

Prototyping a tool environment for run-time assertion checking in JML with communication histories. / Boer, Frank S. de; Gouw, Stijn de; Vinju, Jurgen J.
Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, Maribor, Slovenia, June 22, 2010. New York, NY: ACM Digital Library, 2010. p. 6:1-6:7 6.

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Prototyping a tool environment for run-time assertion checking in JML with communication histories

AU - Boer, Frank S. de

AU - Gouw, Stijn de

AU - Vinju, Jurgen J.

PY - 2010

Y1 - 2010

N2 - In this paper we present prototype tool-support for the runtime assertion checking of the Java Modeling Language (JML) extended with communication histories specified by attribute grammars. Our tool suite integrates Rascal, a meta programming language and ANTLR, a popular parser generator. Rascal instantiates a generic model of history updates for a given Java program annotated with history specifications. ANTLR is used for the actual evaluation of history assertions.

AB - In this paper we present prototype tool-support for the runtime assertion checking of the Java Modeling Language (JML) extended with communication histories specified by attribute grammars. Our tool suite integrates Rascal, a meta programming language and ANTLR, a popular parser generator. Rascal instantiates a generic model of history updates for a given Java program annotated with history specifications. ANTLR is used for the actual evaluation of history assertions.

U2 - 10.1145/1924520.1924526

DO - 10.1145/1924520.1924526

M3 - Conference Article in proceeding

SN - 978-1-4503-0540-2

SP - 6:1-6:7

BT - Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, Maribor, Slovenia, June 22, 2010

PB - ACM Digital Library

CY - New York, NY

T2 - 12th Workshop on Formal Techniques for Java-like Programs

Y2 - 22 June 2010 through 22 June 2010

ER -

Prototyping a tool environment for run-time assertion checking in JML with communication histories

Abstract

Workshop

Access to Document

Fingerprint

Cite this