Stijn de Gouw, Frank S. de Boer, Jurgen J. Vinju. Prototyping a tool environment for run-time assertion checking in JML with Communication Histories. In 12th Workshop on Formal Techniques for Java-like Programs. 2010. [doi]
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.