Home // International Journal On Advances in Software, volume 11, numbers 1 and 2, 2018 // View article

An auto-active approach to develop correct logic-based graph transformations

Authors:
Amani Makhlouf
Christian Percebois
Hanh Nhi Tran

Keywords: Graph transformation; weakest precondition calculus; static analysis; alias calculus; auto-active program verifier

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. 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.

Pages: 147 to 158

Copyright: Copyright (c) to authors, 2018. Used with permission.

Publication date: June 30, 2018

Published in: journal

ISSN: 1942-2628