Engineering Grammar-Based Type Checking for Graph Rewriting Languages

Naoki Yamamoto*, Kazunori Ueda

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract

The ability to handle evolving graph structures is important both for programming languages and modeling languages. Of various languages that adopt graphs as primary data structures, a graph rewriting language LMNtal provides features of both (concurrent) programming languages and modeling languages, and its implementation unifies ordinary program execution and model checking functionalities. Unlike pointer manipulation in imperative languages, LMNtal allows us to manipulate graph structures in such a way that the well-formedness of graphs is guaranteed by the language itself. However, since the shapes of graphs can be complex and diverse compared to algebraic data structures such as lists and trees, it is a non-obvious important task to formulate types of graphs to verify individual programs. With this motivation, this paper discusses LMNtal ShapeType, a type checking framework that applies the basic idea of Structured Gamma to a concrete graph rewriting language. Types are defined by generative grammars written as LMNtal rules, and type checking of LMNtal programs can accordingly be done by exploiting the model checking features of LMNtal itself. We gave a full implementation of type checking exploiting the features of the LMNtal meta-interpreter and confirmed that it works for practical operations on various graph structures, including single-step and multi-step operations on non-algebraic data structures and data structures with numerical shape constraints.

Original languageEnglish
Pages (from-to)114612-114628
Number of pages17
JournalIEEE Access
Volume10
DOIs
Publication statusPublished - 2022

Keywords

  • Dynamic data structures
  • graph grammars
  • graph rewriting
  • type checking

ASJC Scopus subject areas

  • Computer Science(all)
  • Materials Science(all)
  • Engineering(all)
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Engineering Grammar-Based Type Checking for Graph Rewriting Languages'. Together they form a unique fingerprint.

Cite this