up: Publications

# A Hoare-like calculus using the SROIQσ logic on transformations of graphs

### Jon-Hael Brenas, Rachid Echahed, Martin Strecker

TCS 2014

 Abstract

We tackle the problem of partial correctness of programs processing structures defined as graphs. We introduce a kernel imperative programming language endowed with atomic actions that participate in the transformation of graph structures and provide a decidable logic for reasoning about these transformations in a Hoare-style calculus. The logic for reasoning about the transformations (baptized SROIQσ) is an extension of the Description Logic (DL) SROIQ, and the graph structures manipulated by the programs are models of this logic. The programming language is non-standard in that it has an instruction set targeted at graph manipulations (such as insertion and deletion of arcs), and its conditional statements (in loops and selections) are SROIQσ formulas. The main challenge solved in this paper is to show that the resulting proof problems are decidable.

 Online Copy

• Formal development in the Isabelle proof assistant (ongoing)
• A similar framework for the logic ALCQ. The logic is less expressive, but the development is more complete.
 BibTeX Entry
@incollection{brenas14:_hoare_like_calcul_using_sroiq,
author =       {Brenas, Jon Haël and Echahed, Rachid and Strecker, Martin},
title =        {A Hoare-Like Calculus Using the ${\cal SROIQ}^\sigma$ Logic on
Transformations of Graphs},
year =         2014,
isbn =         {978-3-662-44601-0},
booktitle =    {Theoretical Computer Science},
volume =       8705,
series =       {Lecture Notes in Computer Science},
editor =       {Diaz, Josep and Lanese, Ivan and Sangiorgi, Davide},
doi =          {10.1007/978-3-662-44602-7_14},
url =          {https://www.irit.fr/~Martin.Strecker/Publications/tcs2014.html},
publisher =    {Springer Berlin Heidelberg},
keywords =     {Description Logic; Graph Transformation; Programming
Language Semantics; Tableau Calculus},
pages =        {164-178}
}