An Expressive Trace Logic for Recursive Programs

TL;DR

This paper introduces an expressive logic for recursive programs that allows precise specification and reasoning about program traces, establishing a formal connection between programs and logical formulas through a Galois connection.

Contribution

It develops a new trace logic with fixed-points and chop, along with a compositional proof calculus, and demonstrates a formal correspondence between programs and trace formulas.

Findings

Logic is sound and relatively complete for finite-trace properties

Each program can be mapped to a trace formula preserving semantics

Trace formulas can be represented by canonical programs

Abstract

We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.