The graph programming language GP

Graph transformation languages are declarative, rule-based languages that abstract from low-level representations of graphs and graph manipulations. Based on formal rewriting approaches, ~aph transformation languages have a strong formal underpinning which facilitates formal reasoning. However, graph transformation languages that are both expressive enough for elegantly solving complex graph problems and also have a complete formal semantics to facilitate reasoning about programs, are surprisingly rare. In this thesis, we introduce the graph programming language GP (for Graph Programs). GP is a practical graph transformation language with a simple syntax and complete formal semantics that facilitates formal reasoning. GP is a further development of the language presented in [HP01]. We introduce the basis of GP in form of conditional rille schemata [PS04]. The language is based on four core constructs whose semantiCs is defined in the style of Plotkin's structural operational semantics [Plo04]. Practicality and suitability for verification is demonstrated on various case studies in the domain of graph algorithms. The language GP is extended with procedures and parameterised calls to form the language GP+. GP+ provides better structuring of programs and more programming comfort which is demonstrated by a case study on planarity testing.EThOS - Electronic Theses Online ServiceGBUnited Kingdo