Provably Correct Graph Transformations with Small-tALC
Nadezhda Baklanova, Jon Haël Brenas, Rachid Echahed, Christian Percebois, Martin Strecker, Hanh Nhi Tran · 2015
We present a prototype for executing and verifying graph transformations. The transformations are written in a simple imperative programming language, and pre- and post-conditions as well as loop in- variants are specified in the Description Logic ALC (whence the name of the tool). The programming language has a precisely defined oper- ational semantics and a sound Hoare-style calculus. The tool consists of the following sub-components: a compiler to Java for executing the transformations; a verification condition generator; and a tableau prover for an extension of ALC capable of deciding the generated verification conditions. A description of these components and their interaction is the main purpose of this paper.