From Rewriting Logic Executable Semantics to Matching Logic Program Verification

Date Added: Jul 2009
Format: PDF

Rewriting Logic Semantics (RLS) is a definitional framework in which a programming language is defined as a rewrite theory: the algebraic signature defines the program configurations, the equations define structural identities on configurations, and the rewrite rules define the irreversible computational steps. RLS language definitions are efficiently executable using conventional rewrite engines, yielding interpreters for the defined languages for free. Matching logic is a program verification logic inspired by RLS. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Patterns can naturally specify data separation and require no special support from the underlying logic.