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 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. © 2014 IFIP International Federation for Information Processing.