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

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

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.

Read the paper · More papers on PaperTik