Graph Transformation Day (GraTra 01-07)

Wednesday, January 31, 2007 (OAS 3000)

Program

14:00 - 15:00	GP: Language and Environment Detlef Plump, University of York Sandra Steinert, University of York
15:00 - 15:15	Discussion & Coffee Break
15:15 - 16:00	Weakest Preconditions for Graph Programs Karl-Heinz Pennemann, University of Oldenburg
16:00 - 16:15	Discussion & Coffee Break
16:15 - 17:00	Ensuring Formal Correctness of Graph Programs in ENFORCe Karl Azab, University of Oldenburg
17:00 - 17:15	Discussion & Coffee Break
17:15 - 18:00	Autonomous Units with Parallel Process Semantics Hans-Jörg Kreowski, University of Bremen

Abstracts

GP: Language and Environment (Detlef Plump, University of York and Sandra Steinert, University of York)

GP (for Graph Programs) is a rule-based programming language for solving graph problems at a high level of abstraction, freeing programmers from dealing with low-level data structures. The core of GP consists of just three constructs: single-step application of a set of conditional graph-transformation rules, application of a rule set as long as possible, and sequential composition of programs. In this talk, we first discuss a simple program for colouring graphs and then present a formal semantics of GP in the style of structural operational semantics. Besides the core language, the semantics covers powerful new constructs for branching and iteration whose meaning is based on the notion of finitely failing programs. The second part of the talk briefly introduces a concept for recursive procedures in GP. Finally, in the third part, we address the GP environment (graphical editor, compiler and abstract machine) and show how to edit and execute programs.

Weakest Preconditions for Graph Programs (Karl-Heinz Pennemann, University of Oldenburg)

In proof theory, a standard method for showing the correctness of a program with respect to given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. Graph programs are defined by graph transformation rules, sequential composition, nondeterministic choice and iteration as long as possible. In this talk, the notions of graph conditions, rules and programs are (re)introduced, a formal definition of weakest (liberal) preconditions for graph programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented.

Ensuring Formal Correctness of Graph Programs in ENFORCe (Karl Azab, University of Oldenburg)

Graph programs allow a visual description of programs on graphs and graph-like structures. The correctness of a graph program with respect to a pre- and a postcondition can be shown in a classical way by constructing a weakest precondition of the program relative to the postcondition and checking whether the precondition implies the weakest precondition. ENFORCe is a currently developed system for ensuring formal correctness of graph programs and, more general, high-level programs by computing weakest preconditions of these programs. In this talk, we outline the features of the system and present its software framework.

Autonomous Units with Parallel Process Semantics (Hans-Jörg Kreowski, University of Bremen)

Communities of autonomous units are rule-based and graphtransformational devices to model data-processing systems that may consist of distributed and mobile components. The components may communicate and interact with each other, they may link up to ad-hoc networks. In this talk, the parallel-process semantics of communities of autonomous units is introduced and investigated.