# A Hoare-Like Calculus Using the SROIQσ Logic on Transformations of Graphs

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 ${\cal SROIQ}^\sigma$) is an extension of the Description Logic (DL) $\mathcal{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 ${\cal SROIQ}^\sigma$ formulas. The main challenge solved in this paper is to show that the resulting proof problems are decidable.
Keywords :
Type de document :
Communication dans un congrès
Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.164-178, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_14〉
Domaine :

Littérature citée [11 références]

https://hal.inria.fr/hal-01402040
Contributeur : Hal Ifip <>
Soumis le : jeudi 24 novembre 2016 - 10:50:17
Dernière modification le : mercredi 12 septembre 2018 - 17:46:03
Document(s) archivé(s) le : mardi 21 mars 2017 - 02:45:46

### Fichier

978-3-662-44602-7_14_Chapter.p...
Fichiers produits par l'(les) auteur(s)

### Citation

Jon Brenas, Rachid Echahed, Martin Strecker. A Hoare-Like Calculus Using the SROIQσ Logic on Transformations of Graphs. Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.164-178, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_14〉. 〈hal-01402040〉

### Métriques

Consultations de la notice

## 311

Téléchargements de fichiers