A Hoare-Like Calculus Using the SROIQσ Logic on Transformations of Graphs
Résumé
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.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...
