A logic of reachable patterns in linked data-structures (Q2643337): Difference between revisions

A formalism based on the first-order logic over finite graphs with transitive closures is offered for verification of programs with dynamic memory allocation and pointer manipulation. The vocabulary is \(\tau={(C,U,F)}\), where \(C\) is a finite set of constant symbols for designated objects in the heap, pointed to by program variables; \(U\) is a set of unary relation symbols for properties, e.g., the color of a node in a Red-Black tree; \(F\) is a finite set of binary relation symbols for pointer fields. For instance, there can be described a doubly-linked list with forward pointer \(f\) and backward pointer \(b\), pointed to by a program variable \(x\), using the vocabulary with \(C=\{x\}\), \(U=\{\dots \}\), \(F=\{f,b\}\). There can be described a Red-Black tree pointer by a program variable \textit{root} using the vocabulary with \(C= \{\text{\textit{root}}\}\), \({U}= \{\text{red},\text{black}\}\), \(F=\{\text{right},\text{left}\}\). A term \(t\) is either a variable or a constant. An atomic formula is an equality \(t=t'\), a monadic formula \(u(t)\) for \(u\in U\), or an edge formula \({t\overrightarrow{f}t'}\) for some \(f\in F\). A quantifier-free formula \(\psi (v_{0},\dots,v_{n})\) over \(\tau\) with variables \(v_{0},\dots,v_{n}\) is an arbitrary Boolean combination of atomic formulas. A neighbourhood formula \(N(v_{0},\dots,v_{n})\) is a conjunction of edge formulas of the form \(v\overrightarrow{f}v'\), where \(f\in F\), \(v'\in \{v_{0},\dots,v_{n}\}\), and also monadic formulas and their negations. A reachability constraint is a closed formula of the form \(\forall v_{0},\dots,v_{n}\) \(R(c,\dots,v_{0})\Rightarrow (N(v_{0},\dots,v_{n}) \Rightarrow \psi (v_{0},\dots,v_{n}))\), where \(R\) is a routing expression and the conclusion of this formula defines a pattern denoted by \(p(v_{0})\). An \(\mathcal{L}_{0}\) formula is a Boolean combination of reachability constraints. \(\mathcal{L}_{0}\) formulas are interpreted over labeled directed graphs which can be given as finite automata or as regular expressions. The validity problem of \(\mathcal{L}_{0}\) formulas is proved as algorithmically undecidable. Decidable fragments \(\mathcal{L}_{1}\), \(\mathcal{L}_{2}\), \(\mathcal{L}_{3}\) of \(\mathcal{L}_{0}\) are constructed which turned out to be useful for program verification in several interesting cases of verification. Pre-conditions, post-conditions, loop invariants, disjointness of data structures, low-level heap mutations, and an arbitrary number of pointer fields for some interesting programs are expressible in the offered decidable logics, which therefore can be used for automatically proving partial correctness of programs performing low-level heap mutations.