A First-Order Logic with Frames

Lecture notes in computer science, pp. 515–543

Abstract

Abstract We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct $$\textit{Sp}(\cdot )$$ Sp ( · ) that captures the implicit supports of formulas— the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.

Authors 4

1. Adithya Murali

   University of Illinois Urbana-Champaign

   Affiliation as printed

   University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, IL, USA

2. Lucas Peña corresponding

   University of Illinois Urbana-Champaign

   Affiliation as printed

   University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, IL, USA

3. Christof Löding Aachen Department of Computer Science

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Department of Computer Science, Aachen, Germany

4. P. Madhusudan

   University of Illinois Urbana-Champaign

   Affiliation as printed

   University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, IL, USA