A First-order Logic with Frames

Adithya Murali, Lucas Peña, Christof Löding, P. Madhusudan

Research output: Contribution to journalArticlepeer-review

Abstract

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

Original languageEnglish (US)
Article number7
JournalACM Transactions on Programming Languages and Systems
Volume45
Issue number2
DOIs
StatePublished - May 15 2023
Externally publishedYes

Keywords

  • Frame reasoning
  • first-order logic
  • first-order logic with recursive definitions
  • heap verification
  • program logics
  • program verification

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'A First-order Logic with Frames'. Together they form a unique fingerprint.

Cite this