Files in this item



application/pdfMatching Logic - Extended Report.pdf (477kB)
(no description provided)PDF


Title:Matching Logic - Extended Report
Author(s):Rosu, Grigore; Schulte, Wolfram
computer science
Abstract:Hoare logics rely on the fact that logic formulae can encode, or specify, program states, including environments, stacks, heaps, path conditions, data constraints, and so on. Such formula encodings tend to lose the structure of the original program state and thus to be complex in practice, making it difficult to relate formal systems and program correctness proofs to the original programming language and program, respectively. Worse, since programs often manipulate mathematical objects such as lists, trees, graphs, etc., one needs to also encode, as logical formulae, the process of identifying these objects in the encoded program state. This paper proposes matching logic, an alternative to Hoare logics in which the state structure plays a crucial role. Program states are represented as algebraic datatypes called (concrete) configurations, and program state specifications are represented as configuration terms with variables and constraints on them, called (configuration) patterns. A pattern specifies those configurations thatmatch it. Patterns can bind variables to their scope, allowing both for pattern abstraction and for expressing loop invariants. Matching logic is tightly connected to rewriting logic semantics (RLS): matching logic formal systems can systematically be obtained from executable RLS of languages. This relationship allows to prove soundness of matching logic formal systems w.r.t. complementary, testable semantics. All notions are exemplified using KernelC, a fragment of C with dynamic memory allocation/deallocation.
Issue Date:2009-01
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2009-3026
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-23

This item appears in the following Collection(s)

Item Statistics