Hoare-Style Verification of Graph Programs | Zendy

Christopher M. Poskitt | Zendy; Detlef Plump | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Hoare-Style Verification of Graph Programs

Author(s) -

Christopher M. Poskitt,

Detlef Plump

Publication year - 2012

Publication title -

fundamenta informaticae

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.311

H-Index - 67

eISSN - 1875-8681

pISSN - 0169-2968

DOI - 10.3233/fi-2012-708

Subject(s) - hoare logic , computer science , programming language , graph , style (visual arts) , axiomatic semantics , theoretical computer science , semantics (computer science) , operational semantics , correctness , denotational semantics , archaeology , history

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 post-conditions 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research