A Logic for Correlating Temporal Properties across Program Transformations

TL;DR

This paper introduces Temporal Transformation Logic (TTL), a novel logical framework using boolean matrix algebra to verify the correctness of program transformations across different stages, especially in compiler optimizations.

Contribution

It develops TTL with inference rules for various transformations, providing a succinct, constructive, and sound method for reasoning about properties across program transformations.

Findings

TTL effectively models properties of transformed programs.

Boolean matrix algebra simplifies the specification and proof of correctness.

The logic is applicable to compiler optimization verification.

Abstract

Program transformations are widely used in synthesis, optimization, and maintenance of software. Correctness of program transformations depends on preservation of some important properties of the input program. By regarding programs as Kripke structures, many interesting properties of programs can be expressed in temporal logics. In temporal logic, a formula is interpreted on a single program. However, to prove correctness of transformations, we encounter formulae which contain some subformulae interpreted on the input program and some on the transformed program. An example where such a situation arises is verification of optimizing program transformations applied by compilers. In this paper, we present a logic called Temporal Transformation Logic (TTL) to reason about such formulae. We consider different types of primitive transformations and present TTL inference rules for them. Our definitions of program transformations and temporal logic operators are novel in their use of the boolean matrix algebra. This results in specifications that are succinct and constructive. Further, we use the boolean matrix algebra in a uniform manner to prove soundness of the TTL inference rules.