OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

An Auto-active Approach to Develop Correct Logic-based Graph Transformations

Makhlouf, Amani and Percebois, Christian and Tran, Hanh Nhi An Auto-active Approach to Develop Correct Logic-based Graph Transformations. (2018) International Journal on Advances in Software, 11 (1 & 2). 147-158. ISSN 1942-2628

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://www.iariajournals.org/software/tocv11n12.html


We aim at assisting developers to write, in a Hoare style, provably correct graph transformations expressed in the ALCQ Description Logic. Given a postcondition and a transformation rule, we compute the weakest precondition for developers. However, the size and quality of this formula may be complex and hard to grasp. We seek to reduce the weakest precondition’s complexness by a static analysis based on an alias calculus. The refined precondition is presented to the developer in terms of alternative formulae, each one specifying a potential matching of the source graph. By choosing some alternatives that correspond to his intention, the developer can interact with an auto-active program verifier, which continuously ensures the correctness of the resulting Hoare triple.

Item Type:Article
HAL Id:hal-02089337
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:18 Mar 2019 14:40

Repository Staff Only: item control page