Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Expressive Trace Logic for Recursive Programs

Dilian Gurov, Reiner Hähnle

TL;DR

It is shown 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.

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.

An Expressive Trace Logic for Recursive Programs

TL;DR

It is shown 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.

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.

Paper Structure

This paper contains 27 sections, 16 theorems, 18 equations, 6 figures.

Table of Contents

  1. Introduction
  2. The Programming Language Rec
  3. A Denotational Finite-Trace Semantics for Rec
  4. A Logic over Finite Traces
  5. Syntax and Semantics of the Logic
  6. Binary Relations
  7. Strongest Trace Formulas
  8. A Proof Calculus
  9. Definition of the Calculus
  10. Rules
  11. Semantics
  12. Soundness and Relative Completeness of the Calculus
  13. From Trace Formulas to Programs
  14. Rec Programs with Non-deterministic Choice
  15. Canonical Programs
  16. ...and 12 more sections

Key Result

Theorem 8

For all statements $S$ of Rec, we have: $\mathcal{S}_{\mathit{tr}}\!\left[\!\left[S\right]\!\right] \>=\> \mathcal{S}_{\mathit{sos}}\!\left[\!\left[S\right]\!\right]$

Figures (6)

  • Figure 1: SOS rules for Rec.
  • Figure 2: Finite-trace semantic equations for Rec.
  • Figure 3: Finite-trace semantic equations for formulas.
  • Figure 4: Definition of strongest trace formula.
  • Figure 5: The rules of the proof calculus.
  • ...and 1 more figures

Theorems & Definitions (44)

  • Definition 1: Rec Syntax
  • Example 2
  • Example 3
  • Remark 4
  • Definition 5: Rec SOS
  • Definition 6: Induced Finite-Trace Semantics
  • Definition 7: Denotational Finite-Trace Semantics of Rec
  • Theorem 8: Correctness of Trace Semantics
  • Definition 9: Logic Syntax
  • Definition 10: Logic Semantics
  • ...and 34 more