Publication:
Symbolic Animation of JML Specifications

Authors

Thumbnail Image

Permanent Link

https://hdl.handle.net/10289/1520

DOI

10.1007/11526841_7

Publisher link

Rights

Share on Facebook
Share on LinkedIn
Share on X
Share by Email

Abstract

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!

Citation

Fabrice, B., Dadeau, F., Legeard, B. & Utting, M.(2005). Symbolic animation of JML specifications. In Proceeding of International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005(pp. 75-90). Berlin: Springer.

Type

Conference Contribution

Series name

Date

2005

Publisher

Springer

Degree

Type of thesis

Supervisor

DOI

Link to supplementary material

Keywords

computer science, java modelling language, JML, model-based, object-oriented, symbolic animation

Research Projects

Organizational Units

Journal Issue

Collections

Computing and Mathematical Sciences Papers