  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.
