Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, November 24, 2016 - 10:50:17 AM
Last modification on : Monday, July 4, 2022 - 10:08:01 AM
Long-term archiving on: : Tuesday, March 21, 2017 - 2:45:46 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Jon Haël Brenas, Rachid Echahed, Martin Strecker. A Hoare-Like Calculus Using the SROIQσ Logic on Transformations of Graphs. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.164-178, ⟨10.1007/978-3-662-44602-7_14⟩. ⟨hal-01402040⟩



Record views


Files downloads