Portal de Periódicos da CAPES

jmle: A Tool for Executing JML Specifications Via Constraint Programming

2007; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-540-70952-7_19

1611-3349

Ben Krause, Tim Wahls,

Advanced Software Engineering Methodologies

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 a high level of abstraction, and the generated constraint programs are Java implementations of the translated specifications. Hence, they can be called directly from ordinary Java code.