Home // ICSEA 2017, The Twelfth International Conference on Software Engineering Advances // View article

A Precondition Calculus for Correct-by-Construction Graph Transformations

Authors:
Amani Makhlouf
Christian Percebois
Hanh Nhi Tran

Keywords: Graph transformation; Description Logics; weakest precondition calculus; static analysis; alias calculus.

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-by-construction Hoare triple.

Pages: 172 to 177

Copyright: Copyright (c) IARIA, 2017

Publication date: October 8, 2017

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-590-6

Location: Athens, Greece

Dates: from October 8, 2017 to October 12, 2017