Result: JML-testing-tools : A symbolic animator for JML specifications using CLP
Title:
JML-testing-tools : A symbolic animator for JML specifications using CLP
Authors:
Source:
TACAS 2005 : tools and algorithms for the construction and analysis of systems (Edinburgh, 4-8 April 2005)Lecture notes in computer science. :551-556
Publisher Information:
Berlin: Springer, 2005.
Publication Year:
2005
Physical Description:
print, 7 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Logiciel, Software, Génie logiciel, Software engineering, Démonstration automatique, Automatic proving, Demostración automática, Développement logiciel, Software development, Desarrollo logicial, Langage modélisation, Modelling language, Lenguaje modelización, Orienté objet, Object oriented, Orientado objeto, Personnalisation, Customization, Personalización, Programmation logique avec contrainte, Constraint logic programming, Programación lógica con restricción, Raisonnement basé sur modèle, Model-based reasoning, Satisfaction contrainte, Constraint satisfaction, Satisfaccion restricción, Spécification, Specification, Especificación, Validation, Validación
Document Type:
Conference
Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Laboratoire d'Informatique (LIFC), Université de Franche-Comté, CNRS - INRIA, 16, route de Gray, 25030 Besançon, France
ISSN:
0302-9743
Rights:
Copyright 2005 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.16896048
Database:
PASCAL Archive
Further Information
This paper describes a tool for symbolically animating JML specifications using Constraint Logic Programming. A customized solver handles constraints that represent the value of instance fields. We have extended a model-based approach to be able to handle object-oriented specifications. Our tool is also able to check properties during the simulation and exhibit counter-examples for false properties. Therefore, it can be used both for semi-automated verification and for validation purposes.