OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Precondition Calculus for Correct-by-Construction Graph Transformations

Makhlouf, Amani and Percebois, Christian and Tran, Hanh Nhi A Precondition Calculus for Correct-by-Construction Graph Transformations. (2017) In: Twelfth International Conference on Software Engineering Advances (ICSEA 2017), 8 October 2017 - 12 October 2017 (Athens, Greece).

[img]
Preview
(Document in English)

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

Official URL: https://www.thinkmind.org/index.php?view=article&articleid=icsea_2017_8_20_10080

Abstract

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. The developer chooses then the formulae that correspond to his intention to obtain finally a correct-byconstruction Hoare triple.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to International Academy, Research, and Industry Association (IARIA). This papers appears in Proceedings of ICSEA 2017ISSN: 2308-4235 ISBN: 978-1-61208-590-6 The original PDF is available at: https://www.thinkmind.org/index.php?view=article&articleid=icsea_2017_8_20_10080
Audience (conference):International conference proceedings
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:
Statistics:download
Deposited On:19 May 2020 12:48

Repository Staff Only: item control page