jmle: A Tool for Executing JML Specifications Via Constraint Programming

Formal specifications are more useful and easier to develop if they are executable. In this work, we describe a system for executing specifications written in the Java Modeling Language (JML) by translating them to constraint programs, which are then executed via the Java Constraint Kit (JCK). Our system can execute specifications written at evel of abstraction, and the generated constraint programs are Java implementations of the translated specifications. Hence, they can be called directly from ordinary Java code.

• Type: Conference
• Year: 2006
• Where: FMICS
• Authors: Ben Krause, Tim Wahls
• Keywords: Constraint Programs, FMICS 2006, Formal Methods, Java Constraint Kit, Java Modeling Language