Development of Transformation Functions Assisted by a Theorem Prover

Imine Abdessamad; Pascal Molli; Gérald Oster; Michaël Rusinowitch

inria-00107574, version 1

Development of Transformation Functions Assisted by a Theorem Prover

Imine Abdessamad^a^, 1, Pascal Molli ()^b^, 2, Gérald Oster ()^b^, 2, Michaël Rusinowitch^a^, 1

Fourth International Workshop on Collaborative Editing 2002 - ACM CSCW'2002 (2002) 8 p

Résumé : Transformational approach requires to write transformation functions that ensure properties C1 and C2. Proving these conditions on complex typed objects is a serious bottleneck for the application of this approach. We propose to use a theorem prover to assist the development of safe transformation functions. In this paper, we present how we have designed in that way a set of safe transformation functions for an XML typed object.

a – INRIA
b – UNIVERSITE HENRI POINCARE
1 : CASSIS (INRIA Lorraine - LORIA / LIFC)
INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2 : ECOO (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

inria-00107574, version 1
http://hal.inria.fr/inria-00107574
oai:hal.inria.fr:inria-00107574
Contributeur : Publications Loria <>
Soumis le : Jeudi 19 Octobre 2006, 09:01:55
Dernière modification le : Vendredi 20 Octobre 2006, 15:32:31

Voir la fiche détaillée

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Communications avec actes</head>
<biblStruct type="inproceedings" xml:id="inria-00107574"><analytic>
<author><persName><forename>Imine</forename><surname>Abdessamad</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Pascal</forename><surname>Molli</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">ECOO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Gérald</forename><surname>Oster</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">ECOO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Michaël</forename><surname>Rusinowitch</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">Development of Transformation Functions Assisted by a Theorem Prover</title></analytic><monogr><meeting>Fourth International Workshop on Collaborative Editing 2002 - ACM CSCW'2002</meeting><imprint><publisher>none</publisher><pubPlace><settlement>Nouvelle-Orléans</settlement><country> USA</country></pubPlace><biblScope type="publicationDate">2002-00-00</biblScope><biblScope type="pp">8 p</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00107574</idno></biblStruct>
</listBibl>
</listBibl>