Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Hoare-Style Verification of Graph Programs

Poskitt C. M., Plump D.

Fundamenta Informaticae

2012

Vol. 118, nr 1-2

135-175

GP (for Graph Programs) is an experimental nondeterministic programming language for solving problems on graphs and graph-like structures. The language is based on graph transformation rules, allowing visual programming at a high level of abstraction. In particular, GP frees programmers from dealing with low-level data structures. In this paper, we present a Hoare-style proof system for verifying the partial correctness of (a subset of) graph programs. The pre- and postconditions of the calculus are nested graph conditions with expressions, a formalism for specifying both structural graph properties and properties of labels. We show that our proof system is sound with respect to GP’s operational semantics and give examples of its use.

Termination of graph rewriting is undecidable

Plump D.

Fundamenta Informaticae

1998

Vol. 33, nr 2

201-209

It is shown that it is undecidable in general whether a graph rewriting system (in the 'double pushout approach') is terminating. The proof is by a reduction of the Post Correspondence Problem. It is also argued that there is no straightforward reduction of the halting problem for Turing machines or of the termination problem for string rewriting systems to the present problem.