Search

GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with four case studies how programmers can prove termination and partial correctness of their solutions. We argue that GP 2's graph transformation rules, together with induction on the length of program executions, provide a convenient framework for program verification.

GP 2 is an experimental programming language for computing by graph transformation. An initial interpreter for GP 2, written in the functional language Haskell, provides a concise and simply structured reference implementation. Despite its simplicity, the performance of the interpreter is sufficient for the comparative investigation of a range of test programs. It also provides a platform for the development of more sophisticated implementations.

This papers defines the syntax and semantics of GP 2, a revised version of the graph programming language GP. New concepts are illustrated and explained with example programs. Changes to the first version of GP include an improved type system for labels, a built-in marking mechanism for nodes and edges, a more powerful edge predicate for conditional rule schemata, and functions returning the indegree and outdegree of matched nodes. Moreover, the semantics of the branching and loop statement have been simplified to allow their efficient implementation.

GP (for Graph Programs) is a rule-based, nondeterministic programming language for solving graph problems at a high level of abstraction, freeing programmers from handling low-level data structures. The core of GP consists of four constructs: single-step application of a set of conditional graph-transformation rules, sequential composition, branching and iteration. We present a formal semantics for GP in the style of structural operational semantics. A special feature of our semantics is the use of finitely failing programs to define GP's powerful branching and iteration commands.