# A First-Order Logic with Frames

## TL;DR

Frame Logic (FL) is a new logical framework that extends first-order logic with support constructs, enabling elegant reasoning about models and programs that involve dynamic updates and local specifications.

## Contribution

The paper introduces Frame Logic, a novel extension of first-order logic with support constructs, and demonstrates its expressiveness and applicability to program reasoning and separation logic.

## Key findings

- Captures data-structures using FL.
- Provides translation from separation logic fragment to FL.
- Designs a program logic based on FL for heap updates.

## Abstract

We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct 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.