Symbolic Animation of JML Specifications - Archive ouverte HAL Access content directly
Conference Papers Year : 2005

Symbolic Animation of JML Specifications

(1) , (1) , (1) , (2)


This paper presents a model-based framework for the symbolic animation of object-oriented specifications. A customized set-theoretic solver is used to simulate the execution of the system and handle constraints on state variables. We define a framework for animating object-oriented specifications with dynamic object creations, interactions and inheritance. We show how this technique can be applied to Java Modeling Language (JML) specifications, making it possible to animate Java programs that only contain method interfaces and no code!

Dates and versions

inria-00329983 , version 1 (13-10-2008)



Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Marc Utting. Symbolic Animation of JML Specifications. International Conference on Formal Methods - FM'05, Jul 2005, Newcastle upon Tyne, United Kingdom. pp.75-90, ⟨10.1007/b27882⟩. ⟨inria-00329983⟩
100 View
0 Download



Gmail Facebook Twitter LinkedIn More