An Expressive Trace Logic for Recursive Programs

It is uncommon that specification languages used in program verification are as expressive as the programs they are intended to specify: In model checking [7] one typically abstracts away from data and unwinds unbounded control structures. Specification of unbounded computations is achieved by recursively defined temporal operators. In deductive verification [15], first-order Hoare-style contracts [18] are the basis of widely used specification languages [3, 22]. The latter specify computation by taking symbolic memory snapshots in terms of first-order formulas, typically at the beginning and at the end of unbounded control structures, such as procedure call and return, or upon loop entry and exit. Contracts permit to approximate the effect of unbounded computation as a finite number of first-order formulas against which a program’s behavior can be verified.

Imagine, in contrast, a logic for program specification that is at least as expressive as the programs it is supposed to describe. Formulas $\varphi$ of such a logic characterize a generally infinite set of program computation traces $\sigma$. One can then form judgments of program statements $S$ of the form $S:\varphi$ with the natural semantics that any possible trace $\sigma$ of $S$ is one of the traces described by $\varphi$.

Two arguments against such a trace logic are easily raised: first, one expects a specification language to be capable of abstraction from implementation details; second, its computational complexity. Regarding the first, we note that any desired degree of abstraction can be achieved by definable constructs, i.e. syntactic sugar, in a sufficiently rich trace logic. Regarding the second, it is far from obvious whether the computational worst-case tends to manifest itself in practical verification [15]. First experiments seem to indicate this is not the case. On the other hand, a rich, trace-based specification logic bears many advantages:

1. 1.

   On the practical side, trace-based specification permits to express, for example, that an event or a call happened (exactly once, at least once) or that did not happen. Likewise, one can specify without reference to the target code (via assertions) that a condition holds at some point which is not necessarily an endpoint of a procedure call. It is also possible to specify inter-procedural properties, such as call sequences, absence of callbacks, etc. Such properties are important in security analysis and they are difficult or impossible to express with Hoare-style contracts or in temporal logic.

2. 2.

   The semantics of trace formulas in terms of trace sets can be closely aligned with a suitable program semantics, which greatly simplifies soundness and completeness proofs.

3. 3.

   An expressive trace logic makes for simple and natural completeness proofs for judgments $S:\varphi$, because it is unnecessary to encode the program semantics in order to construct sufficiently strong first-order conditions.

4. 4.

   In a calculus for judgments of the form $S:\varphi$, one can design inference rules that directly decompose judgments into simpler ones, but also algebraic rules that simplify and transform $\varphi$, and one may mix both reasoning styles.

5. 5.

   The semantics of programs, of trace formulas, and the rules of the calculus can be formulated in a fully compositional manner: definitions and inference rules involve no intermediate state or context.

6. 6.

   In consequence, we are able to establish a close correspondence between programs and formulas, which sheds light on the exact relation between each program construct and its corresponding logical connective. We formulate and prove a Galois connection that formalizes this fact.

Our main contribution is a trace logic for imperative programs with recursive procedures where we formalize and prove the claims above. We restrict attention to the terminating executions of programs, i.e. to their finite trace semantics. This is not a fundamental limitation, but the desire not to obscure the construction with complications that may be added later. Still, adaptating the theory to maximal traces (including infinite runs) is not trivial, and working out the details is left as future work (see Section 8.3).

Our paper is structured as follows: In Section 2 we define the programming language Rec used throughout this paper and we give it a standard SOS semantics [29]. In Section 3 we define a denotational semantics for Rec in fully compositional style and prove it equivalent to the SOS semantics. In Section 4 we introduce our trace logic and map programs to formulas by the concept of a strongest trace formula, which is shown to fully preserve program semantics. In Section 5 we define a proof calculus for judgments and show it to be sound and complete. In Section 6, using the concept of a canonical program, we map trace formulas back to programs in the slightly extended language ${\text{Rec}}^{\ast }$ with non-deterministic guards. We prove that ${\text{Rec}}^{\ast }$ and trace formulas form a Galois connection via strongest trace formulas and canonical programs. In Section 7 we discuss related work, in Section 8 we sketch some extensions, including options to render specifications more abstract and how to prove consequence among trace formulas. In Section 9 we conclude.

All proofs and some examples can be found in the accompanying report [14]. The most important of these are also available in the present Appendix.

We define a simple programming language Rec with recursive procedures and give it a standard SOS semantics. We follow the notation of [26], adapted to Rec syntax.

A standard, structural operational semantics (SOS) for Rec is defined in Figure 1 (sometimes referred to as small-step semantics). We use it as a baseline when defining the denotational finite-trace semantics in Section 3.

Let $\mathrm{𝑉𝑎𝑟}$ be the set of program variables, and State the set of program states $s:\mathrm{𝑉𝑎𝑟}\to \mathbb{Z}$. Let $𝒜\left[\left[a\right]\right](s)\in \mathbb{Z}$ denote the integer value of the arithmetic expression $a$ when evaluated in state $s$, and $ℬ\left[\left[b\right]\right](s)\in 𝕋$ denote the truth value of the Boolean expression $b$ when evaluated in state $s$, both defined as expected.

A configuration is either a pair consisting of a statement and a state, designating an initial or intermediate configuration; or a state $s$, designating a final configuration. To simplify notation we assume that $S$ is evaluated relative to a Rec program with a procedure table $T$ which is not explicitly specified.

The transitions of the SOS either relate two intermediate configurations, or an intermediate with a final one, and thus have the shape or , respectively.

The structural operational semantics of Rec induces a finite-trace semantics in terms of the sequences of states that are traversed from an initial to a final configuration when executing a given statement in the SOS. Let ${\text{State}}^{+}$ denote the set of all non-empty, finite sequences of states. Formally, we define a function ${𝒮}_{\mathrm{𝑠𝑜𝑠}}\left[\left[S\right]\right]:\text{Stm}\to 2^{{\text{State}}^{+}}$, i.e., a function such that ${𝒮}_{\mathrm{𝑠𝑜𝑠}}\left[\left[S\right]\right]\subseteq {\text{State}}^{+}$ for any statement $S$.

Observe that in Definition 2.6 any state $s_0\in \text{State}$ can serve as the initial state of a finite trace. Next we design a “direct-style”, denotational finite-trace semantics that conforms with the SOS, in the sense that it is equal to the finite-trace semantics induced by the SOS.

We define the semantic function ${𝒮}_{\mathrm{𝑡𝑟}}:\text{Stm}\to 2^{{\text{State}}^{+}}$ with the intention that ${𝒮}_{\mathrm{𝑡𝑟}}\left[\left[S\right]\right]={𝒮}_{\mathrm{𝑠𝑜𝑠}}\left[\left[S\right]\right]$. Unlike ${𝒮}_{sos}$, however, ${𝒮}_{\mathrm{𝑡𝑟}}$ is defined directly, without referring to other semantic rules as SOS does (hence the term “direct-style”). We define ${𝒮}_{\mathrm{𝑡𝑟}}\left[\left[S\right]\right]$ in the style of denotational semantics, compositionally, by induction on the structure of $S$, and through defining equations. We let $\sigma$ range over traces.

Let us define a unary restriction operator on trace sets, for any trace set $A$ and Boolean expression $b\in \text{BExp}$, as follows: . It filters out all traces in $A$ whose first state does not satisfy $b$. Another unary operator on trace sets is defined as $\mathrm{♯}A\stackrel{\mathrm{𝖽𝖾𝖿}}{=}\left\{s\cdot s\cdot \sigma \right|s\cdot \sigma \in A\}$ which duplicates the first state in each trace in $A$. Finally, let us define the binary operator on trace sets: $A⌢B\stackrel{\mathrm{𝖽𝖾𝖿}}{=}\left\{{\sigma }_A\cdot s\cdot {\sigma }_B\right|{\sigma }_A\cdot s\in A\wedge s\cdot {\sigma }_B\in B\}$ which concatenates traces from $A$ with traces from $B$ that agree on the last and first state, respectively, but without duplicating that state, see also [16].

The finite-trace semantics agrees with the SOS of Rec, in the sense that ${𝒮}_{\mathrm{𝑡𝑟}}\left[\left[S\right]\right]$ coincides with the finite-trace semantics ${𝒮}_{\mathrm{𝑠𝑜𝑠}}\left[\left[S\right]\right]$ induced by the SOS, as defined in Definition 2.6.

Our trace logic can be seen as an Interval Temporal Logic [16] with $\mu$-recursion [28], or alternatively, as a temporal $\mu$-calculus with a binary temporal operator corresponding to the chop operation over sets of traces (see, e.g., [32] for a general introduction to $\mu$-calculus).

We present a proof calculus for our logic in the form of a Gentzen-style deductive proof system, which is compositional both in the statement and the formula.

In Section 4.3 we showed that any Rec program $S$ can be translated into a trace formula $\mathrm{𝗌𝗍𝖿}(S)$ that has the same semantics in terms of traces. Now we look at the other direction: Given a trace formula $\varphi$, can we construct a canonical program $\mathrm{𝖼𝖺𝗇}(\varphi )$ that has the same semantics in terms of traces? In general, this is not possible, as the following example shows:

We do not discuss higher-order logical frameworks [4, 27], because they serve a different purpose: Their expressiveness can be used to mechanize verification frameworks, including syntax, semantics, and calculus. For example, a mechanization of contract-based deductive verification is in [34]. One could do that also for the approach in the present paper.

Stirling [32, p. 528, footnote 2] suggests that the $\mu$-calculus can be generalized to non-unary predicates, but does not develop this possibility further. In [24], Müller-Olm proposes a modal fixed point logic with chop, which can characterize any context-free process up to bisimulation or simulation. The logic is shown to be strictly more expressive than the modal $\mu$-calculus. Lange & Somla [21] relate propositional dynamic logic over context-free programs with Müller-Olm’s logic and show the former to be equi-expressive with a fragment of the latter. Fredlund et al. [13] present a verification tool for the Erlang language based on first-order $\mu$-calculus with actions [9]. Rosu et al. [6, 31] propose matching logic (ML) as a unifying logic for specifying and reasoning about the static structure and dynamic behaviour of programs. It uses patterns and constraints to uniformly represent mathematical domains, data types, and transition systems, whose properties can be reasoned about using one proof system. Our trace logic bares certain similarities with ML, both allowing recursion, but our logic is syntax-driven and has a fixed semantics in the domain of program traces, while ML is a semantic approach. We are not aware of a similar result as Corollary 6.8 in ML.

In contrast to the above mentioned work, we separate programs from fixed point formulas, and relate them in the form of judgments. Our logic has a single binary operator ${\mathrm{𝑆𝑏}}_x^a$ over arithmetic expressions $a$ and program variables $x$, together with the chop operator $⌢$. The latter models composition of binary relations in the denotational semantics. Our logic is sufficient to characterize any Rec program. Specifically, $\mu$-formulas can serve as contracts of recursive procedures. More importantly, our approach leads to a compositional calculus, where all rules but the consequence rule are analytic.

Kleene algebra with tests (KAT) [19] are an equational algebraic theory that has been shown to be as expressive as propositional while programs. They were mechanized in an interactive theorem prover [30] and are able to express at least Hoare-style judgments [20]. The research around KATs focuses on propositional while programs: we are not aware of results relating KAT with recursive stateful programs. Specifically, our result that procedure contracts can be expressed purely in terms of trace formulas (Theorem 4.8) has not been obtained by algebraic approaches.

Expressive trace-based specification languages are rare in program verification. The trace logic of Barthe et al. [2] is a many-sorted first-order logic, equipped with an arithmetic theory of explicit trace positions to define program semantics. It is intended to model program verification in first-order logic for processing in automated theorem provers. Like ${𝒮}_{\mathrm{𝑡𝑟}}\left[\left[\right]\right]$, their program semantics is compositional; however, it uses explicit time points instead of algebraic operators. An extension of Hoare logic with trace specifications is presented by Ernst et al. [11]. Hoare triples are extended with regular expressions recording events emitted before the execution of the command and the events emitted by its execution. Our trace logic is more expressive. Also the first-order temporal logic of nested words (NWTL) of Alur et al. [1] permits to specify certain execution patterns within symbolic traces. It is orthogonal to our approach, being based on nested event pairs and temporal operators, instead of least fixed points and chop. NWTL is equally expressive over nested words as first-order logic. The intended computational model is not Rec, but non-deterministic Büchi automata over nested words for which it is complete. Temporal stream logic of Finkbeiner et al. [12], like our trace logic, has state updates ${\mathrm{𝑆𝑏}}_x^t$ (with a different syntax) and state predicates, but it is based on linear temporal logic and has no fixed points or chop. Again, the intended computational model is an extension of Büchi automata, the verification target are FPGA programs.

Cousot & Cousot [8] define a trace-based semantics for modal logics where (infinite) traces are equipped with past, present, and future. Their main focus is to relate model checking and static analysis to abstract interpretation – the trace-based semantics is the basis for it. In contrast, our paper relates a computation model to a logic. Like our semantics, theirs is compositional and the operators mentioned in their paper could inspire abstractions of our trace logic, cf. Section 8.1 below.

Nakata & Uustalu [25] present a trace-based co-inductive operational semantics with chop for an imperative programming language with loops. Following up on this work, [10] extended the approach to an asynchronous concurrent language, but neither of these uses fixed points, so that the specification language is incomplete. Also the calculus is not compositional.

Closest to the present work is our earlier work on trace-based deductive verification [5], where we used a similar trace logic than here. However, neither the semantics nor the calculus were compositional. Furthermore, we proved soundness there, but left completeness as an open question.

We presented a fixed point logic that characterizes recursive programs with non-deterministic guards. Both, programs and formulas have the same kind of trace semantics, which, like the calculus for proving judgments, is fully compositional in the sense that the definitions and rules embody no context. The faithful embedding of programs into a logic seems to suggest that we merely replace one execution model (programs) with another (trace formulas). So why is it worth having such an expressive specification logic? We can see four reasons:

First, the logic renders itself naturally to extension and abstraction that cannot be easily mimicked by programs or that are much less natural for programs. This is corroborated by the discussion in Section 8.1, but also by the case of conjunction: It is trivial to add conjunction $\varphi \wedge \psi$ to the trace logic and to a calculus for trace formulas, but conjunction has no natural program counter-part. Yet it permits to specify certain hyper-properties, i.e., properties relating sets of traces.

Second, the logic offers reasoning patterns that are easily justified algebraically, such as projection, replacement of equivalents, strengthening, distribution, etc., that are not obvious in the realm of programs.

Third, the concept of strongest trace formula leads to a characterization of valid judgments and, thereby, enables a simple completeness proof.

And finally, the duality between programs and formulas permits to prove judgments by freely mixing two styles of reasoning: with the rules of the calculus in Figure 5, or using a calculus for the consequence of trace formulas. For example, a judgment such as $\mathrm{𝑑𝑜𝑤𝑛}():\mathrm{𝐼𝑑}⌢{\mathrm{𝐷𝑒𝑐}}_x^{+}$ can be proved as in Example 8.1 or directly with the rules in Figure 5, but also by mixing both styles.

A perhaps surprising feature of our trace logic is the fact that no explicit notion of procedure contract is required to achieve procedure-modular verification: Instead, strongest trace formulas and statement variables are employed. This results in a novel (Call) rule that works with symbolic continuations realized by statement variables.