A Hoare-like calculus using the SROIQσ logic on transformations of graphs
Jon-Hael Brenas, Rachid Echahed, Martin Strecker
TCS 2014
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.
- 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.
@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 = {http://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}
}
Last modified: Mon Sep 1 10:07:21 CEST 2014
|