Verified Self-Explaining Computation

TL;DR

This paper introduces a formal framework for verifying dynamic program slicing algorithms, demonstrating their duality through proof assistant verification, advancing the reliability of program analysis tools.

Contribution

It formalizes and verifies the duality of forward and backward dynamic slicing algorithms within a simple imperative language using Coq.

Findings

Formal proof of duality between slicing algorithms

Verification of slicing algorithms in Coq

Enhanced understanding of dynamic analysis correctness

Abstract

Common programming tools, like compilers, debuggers, and IDEs, crucially rely on the ability to analyse program code to reason about its behaviour and properties. There has been a great deal of work on verifying compilers and static analyses, but far less on verifying dynamic analyses such as program slicing. Recently, a new mathematical framework for slicing was introduced in which forward and backward slicing are dual in the sense that they constitute a Galois connection. This paper formalises forward and backward dynamic slicing algorithms for a simple imperative programming language, and formally verifies their duality using the Coq proof assistant.

Figures

Equations

$$[\text{x}\mapsto \square ,\text{y}\mapsto 1,\text{z}\mapsto \square ]$$

$$\mu =[\text{x}\mapsto 1,\text{y}\mapsto \square ]$$

$$\frac{}{\square ⊑a}\frac{}{n⊑n}\frac{}{x⊑x}\frac{a_1⊑a_1^{\prime }{a}_2⊑a_2^{\prime }}{a_1+a_2⊑a_1^{\prime }+a_2^{\prime }}$$

$$a\bigsqcup \square =a\square \bigsqcup a=an\bigsqcup n=nx\bigsqcup x=x$$

$$(a_1+a_2)\bigsqcup (a_1^{\prime }+a_2^{\prime })=(a_1\bigsqcup a_1^{\prime })+(a_2\bigsqcup a_2^{\prime })$$

$$(a_1,b_1)⊑(a_2,b_2)⟺a_1⊑a_2\wedge b_1⊑b_2$$

$${\forall }_{q\in Q}f(g(q)){⊑}_{Q}q$$

$${\forall }_{p\in P}p{⊑}_{P}g(f(p))$$

$$\dfrac{}{\mu,n\Rightarrow{\color[rgb]{0.5,0.5,0.5}n::\ }v_{n}}\;\;\;\;\;\;\dfrac{\mu(x)=v_{a}}{\mu,x\Rightarrow{\color[rgb]{0.5,0.5,0.5}x(v_{a})::\ }v_{a}}\;\;\;\;\;\;\dfrac{\mu,a_{1}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }v_{1}\;\;\;\;\;\;\mu,a_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }v_{2}}{\mu,a_{1}+a_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}+T_{2}::\ }v_{1}+_{\mathbb{N}}v_{2}}$$

$$\dfrac{}{\mu,\texttt{true}\Rightarrow{\color[rgb]{0.5,0.5,0.5}\texttt{true}::\ }\textsf{true}}\;\;\;\;\;\;\dfrac{}{\mu,\texttt{false}\Rightarrow{\color[rgb]{0.5,0.5,0.5}\texttt{false}::\ }\textsf{false}}$$

$$\dfrac{\mu,a_{1}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }v_{1}\;\;\;\;\;\;\mu,a_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }v_{2}}{\mu,a_{1}=a_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}=T_{2}::\ }v_{1}=_{\mathbb{B}}v_{2}}\;\;\;\dfrac{\mu,b\Rightarrow{\color[rgb]{0.5,0.5,0.5}T::\ }v}{\mu,\neg b\Rightarrow{\color[rgb]{0.5,0.5,0.5}\neg T::\ }\neg_{\mathbb{B}}v}$$

$$\dfrac{\mu,b_{1}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }v_{1}\;\;\;\;\;\;\mu,b_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }v_{2}}{\mu,b_{1}\wedge b_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}\wedge T_{2}::\ }v_{1}\wedge_{\mathbb{B}}v_{2}}$$

$$\dfrac{}{\mu,\texttt{skip}\Rightarrow{\color[rgb]{0.5,0.5,0.5}\texttt{skip}::\ }\mu}\;\;\;\;\;\;\dfrac{\mu,a\Rightarrow_{a}{\color[rgb]{0.5,0.5,0.5}T_{a}::\ }v_{a}\;\;\;\;\;\;}{\mu,x:=a\Rightarrow{\color[rgb]{0.5,0.5,0.5}x:=T_{a}::\ }\mu[x\mapsto v_{a}]}$$

$$\dfrac{\mu,c_{1}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }\mu^{\prime}\;\;\;\;\;\;\mu^{\prime},c_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }\mu^{\prime\prime}}{\mu,c_{1}\,;\,c_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}\,;\,T_{2}::\ }\mu^{\prime\prime}}$$

$$\dfrac{\mu,b\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{b}::\ }\textsf{\small{true}}\;\;\;\;\;\;\mu,c_{1}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }\mu^{\prime}}{\mu,\texttt{if}\;b\;\texttt{then}\;\{\;c_{1}\;\}\;\texttt{else}\;\{\;c_{2}\;\}\Rightarrow{\color[rgb]{0.5,0.5,0.5}\texttt{if}_{\textsf{true}}\;T_{b}\;\texttt{then}\;\{\;T_{1}\;\}::\ }\mu^{\prime}}$$

$$\dfrac{\mu,b\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{b}::\ }\textsf{\small{false}}\;\;\;\;\;\;\mu,c_{2}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }\mu^{\prime}}{\mu,\texttt{if}\;b\;\texttt{then}\;\{\;c_{1}\;\}\;\texttt{else}\;\{\;c_{2}\;\}\Rightarrow{\color[rgb]{0.5,0.5,0.5}\texttt{if}_{\textsf{false}}\;T_{b}\;\texttt{else}\;\{\;T_{2}\;\}::\ }\mu^{\prime}}$$

$$\dfrac{\mu,b\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{b}::\ }\textsf{\small{false}}}{\mu,\texttt{while}\;b\;\texttt{do}\;\{\;c\;\}\Rightarrow{\color[rgb]{0.5,0.5,0.5}\texttt{while}_{\textsf{false}}\;T_{b}::\ }\mu}$$

$$\dfrac{\mu,b\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{b}::\ }\textsf{\small{true}}\;\;\;\;\;\;\mu,c\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{c}::\ }\mu^{\prime}\;\;\;\;\;\;\mu^{\prime},\texttt{while}\;b\;\texttt{do}\;\{\;c\;\}\Rightarrow{\color[rgb]{0.5,0.5,0.5}T_{w}::\ }\mu^{\prime\prime}}{\mu,\texttt{while}\;b\;\texttt{do}\;\{\;c\;\}\Rightarrow{\color[rgb]{0.5,0.5,0.5}\texttt{while}_{\textsf{true}}\;T_{b}\;\texttt{do}\;\{\;T_{c}\;\};\;T_{w}::\ }\mu^{\prime\prime}}$$

$$\dfrac{}{{\color[rgb]{0.5,0.5,0.5}T::\ }\mu,\Box\nearrow\Box}\;\;\;\;\;\;\dfrac{}{{\color[rgb]{0.5,0.5,0.5}n::\ }\mu,n\nearrow n}\;\;\;\;\;\;\dfrac{}{{\color[rgb]{0.5,0.5,0.5}x(v_{a})::\ }\mu,x\nearrow\mu(x)}$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }\mu,a_{1}\nearrow\Box}{{\color[rgb]{0.5,0.5,0.5}T_{1}+T_{2}::\ }\mu,a_{1}+a_{2}\nearrow\Box}\;\;\;\;\;\;\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }\mu,a_{2}\nearrow\Box}{{\color[rgb]{0.5,0.5,0.5}T_{1}+T_{2}::\ }\mu,a_{1}+a_{2}\nearrow\Box}$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }\mu,a_{1}\nearrow v_{1}\;\;\;\;\;\;{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }\mu,a_{2}\nearrow v_{2}}{{\color[rgb]{0.5,0.5,0.5}T_{1}+T_{2}::\ }\mu,a_{1}+a_{2}\nearrow v_{1}+_{\mathbb{N}}v_{2}}\;\;\;v_{1},v_{2}\neq\Box$$

$$\dfrac{}{{\color[rgb]{0.5,0.5,0.5}T::\ }\mu,\Box\nearrow\Box}$$

$$\dfrac{}{{\color[rgb]{0.5,0.5,0.5}\texttt{true}::\ }\mu,\texttt{true}\nearrow\textsf{\small{true}}}\;\;\;\;\;\;\dfrac{}{{\color[rgb]{0.5,0.5,0.5}\texttt{false}::\ }\mu,\texttt{false}\nearrow\textsf{\small{false}}}$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }a_{1}\nearrow\Box}{{\color[rgb]{0.5,0.5,0.5}T_{1}=T_{2}::\ }\mu,a_{1}=a_{2}\nearrow\Box}\;\;\;\;\;\;\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }a_{2}\nearrow\Box}{{\color[rgb]{0.5,0.5,0.5}T_{1}=T_{2}::\ }\mu,a_{1}=a_{2}\nearrow\Box}$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }a_{1}\nearrow v_{1}\;\;\;\;\;\;{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }a_{2}\nearrow v_{2}}{{\color[rgb]{0.5,0.5,0.5}T_{1}=T_{2}::\ }\mu,a_{1}=a_{2}\nearrow v_{1}=_{\mathbb{B}}v_{2}}\;\;\;v_{1},v_{2}\neq\Box$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T::\ }b\nearrow\Box}{{\color[rgb]{0.5,0.5,0.5}\neg T::\ }\mu,\neg b\nearrow\Box}\;\;\;\;\;\;\dfrac{{\color[rgb]{0.5,0.5,0.5}T::\ }b\nearrow v_{b}}{{\color[rgb]{0.5,0.5,0.5}\neg T::\ }\mu,\neg b\nearrow\neg_{\mathbb{B}}v}\;\;\;v_{b}\neq\Box$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }b_{1}\nearrow\Box}{{\color[rgb]{0.5,0.5,0.5}T_{1}\wedge T_{2}::\ }\mu,b_{1}\wedge b_{2}\nearrow\Box}\;\;\;\;\;\;\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }b_{2}\nearrow\Box}{{\color[rgb]{0.5,0.5,0.5}T_{1}\wedge T_{2}::\ }\mu,b_{1}\wedge b_{2}\nearrow\Box}$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }b_{1}\nearrow v_{1}\;\;\;\;\;\;{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }b_{2}\nearrow v_{2}}{{\color[rgb]{0.5,0.5,0.5}T_{1}\wedge T_{2}::\ }\mu,b_{1}\wedge b_{2}\nearrow v_{1}\wedge_{\mathbb{B}}v_{2}}\;\;\;v_{1},v_{2}\neq\Box$$

$$\dfrac{}{{\color[rgb]{0.5,0.5,0.5}\texttt{skip}::\ }\mu,\Box\nearrow\mu}\;\;\;\;\;\;\dfrac{}{{\color[rgb]{0.5,0.5,0.5}\texttt{skip}::\ }\mu,\texttt{skip}\nearrow\mu}\;\;\;\;\;\;\dfrac{}{{\color[rgb]{0.5,0.5,0.5}x:=T_{a}::\ }\mu,\Box\nearrow\mu[x\mapsto\Box]}$$

$$\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{a}::\ }\mu,a\nearrow v_{a}}{{\color[rgb]{0.5,0.5,0.5}x:=T_{a}::\ }\mu,x:=a\nearrow\mu[x\mapsto v_{a}]}\;\;\;\;\;\;\dfrac{{\color[rgb]{0.5,0.5,0.5}T_{1}::\ }\mu,\Box\nearrow\mu^{\prime}\;\;\;\;\;\;{\color[rgb]{0.5,0.5,0.5}T_{2}::\ }\mu^{\prime},\Box\nearrow\mu^{\prime\prime}}{{\color[rgb]{0.5,0.5,0.5}T_{1}\,;\,T_{2}::\ }\mu,\Box\nearrow\mu^{\prime\prime}}$$

Full text

1 Introduction

The aim of mathematical program construction is to proceed from (formal) specifications to (correct) implementations. For example, critical components such as compilers, and various static analyses they perform, have been investigated extensively in a formal setting [10]. However, we unfortunately do not yet live in a world where all programs are constructed in this way; indeed, since some aspects of programming (e.g. exploratory data analysis) appear resistant to a priori specification, one could debate whether such a world is even possible. In any case, today programs “in the wild” are not always mathematically constructed. What do we do then?

One answer is provided by a class of techniques aimed at explanation, comprehension or debugging, often based on run-time monitoring, and sometimes with a pragmatic or even ad hoc flavour. In our view, the mathematics of constructing well-founded (meta)programs for explanation are wanting [4]. For example, dynamic analyses such as program slicing have many applications in comprehending and restructuring programs, but their mathematical basis and construction are far less explored compared to compiler verification [2, 3].

Dynamic program slicing is a runtime analysis that identifies fragments of a program’s input and source code – known together as a program slice – that were relevant to producing a chosen fragment of the output (a slicing criterion) [8, 21]. Slicing has a very large literature, and there are a wide variety of dynamic slicing algorithms. Most work on slicing has focused on imperative or object-oriented programs.

One common application of dynamic slicing is program debugging. Assume we have a program with variables x, y, and z and a programmer expects that after the program has finished running these variables will have respective values 1, 2, and 3. If a programmer unfamiliar with the program finds that after execution, variable y contains 1 where she was expecting another value, she may designate y as a slicing criterion, and dynamic slicing will highlight fragments of the source code that could have contributed to producing the incorrect result. This narrows down the amount of code that the programmer needs to inspect to correct a program. In this tiny example, of course, there is not much to throw away and the programmer can just inspect the program — the real benefit of slicing is for understanding larger programs with multiple authors. Slicing can also be used for program comprehension, i.e. to understand the behaviour of an already existing program in order to re-engineer its specification, possibly non-existent or not up-to-date.

In recent years a new semantic basis for dynamic slicing has been proposed [15, 17]. It is based on the concept of Galois connections as known from order and lattice theory. Given lattices $X$ and $Y$, a Galois connection is a pair of functions $g:Y\to X$ and $f:X\to Y$ such that $g(y)\leq x\iff y\leq f(x)$; then $g$ is the lower adjoint and $f$ is the upper adjoint. Galois connections have been advocated as a basis for mathematical program construction already, for example by Backhouse [1] and Mu and Oliveira [12]. They showed that if one can specify a problem space and show that it is one of the component functions of a Galois connection (the “easy” part), then optimal solutions to the problem (the “hard” part) are uniquely determined by the dual adjoint. A simple example arises from the duality between integer multiplication and division: the Galois connection $x\cdot y\leq z\iff x\leq z/y$ expresses that $z/y$ is the greatest integer such that $(z/y)\cdot y\leq z$.

Whereas Galois connections have been used previously for constructing programs (as well as other applications such as program analysis), here we consider using Galois connections to construct programs for program slicing. In our setting, we consider lattices of partial inputs and partial outputs of a computation corresponding to possible input and output slicing criteria, as well as partial programs corresponding to possible slices—these are regarded as part of the input. We then define a forward semantics (corresponding to forward slicing) that expresses how much of the output of a program can be computed from a given partial input. Provided the forward semantics is monotone and preserves greatest lower bounds, it is the upper adjoint of a Galois connection, whose lower adjoint computes for each partial output the smallest partial input needed to compute it — which we consider an explanation. In other words, forward and backward slicing are dual in the sense that forward slicing computes “as much as possible” of the output given a partial input, while backward slicing computes “as little as needed” of the input to recover a partial output.

Figure 1 illustrates the idea for a small example where the “program” is an expression $(x+y,2x)$, the input is an initial store containing $[x=1,y=2]$ and the output is the pair $(3,2)$. Partial inputs, outputs, and programs are obtained by replacing subexpressions by “holes” ($\Box$), as illustrated via (partial) lattice diagrams to the left and right. In the forward direction, computing the first component succeeds if both $x$ and $y$ are available while the second component succeeds if $x$ is available; the backward direction computes the least input and program slice required for each partial output. Any Galois connection induces two isomorphic sublattices of the input and output, and in Figure 1 the elements of these sublattices are enclosed in boxes with thicker lines. In the input, these elements correspond to minimal explanations: partial inputs and slices in which every part is needed to explain the corresponding output. The corresponding outputs are maximal in a sense that their minimal explanations do not explain anything else in the output.

The Galois connection approach to slicing has been originally developed for functional programming languages [15] and then extended to functional languages with imperative features [17]. So far it has not been applied to conventional imperative languages, so it is hard to compare directly with conventional slicing techniques. Also, the properties of the Galois connection framework in [15, 17] have only been studied in pen-and-paper fashion. Such proofs are notoriously tricky in general and these are no exception; therefore, fully validating the metatheory of slicing based on Galois connections appears to be an open problem.

In this paper we present forward and backward slicing algorithms for a simple imperative language Imp and formally verify the correctness of these algorithms in Coq. Although Imp seems like a small and simple language, there are nontrivial technical challenges associated with slicing in the presence of mutable state, so our formalisation provides strong assurance of the correctness of our solution. To the best of our knowledge, this paper presents the first formalisation of a Galois connection slicing algorithm for an imperative language. Compared with Ricciotti et al. [17], Imp is a much simpler language than they consider, but their results are not formalised; compared with Léchenet et al. [9], we formalise dynamic rather than static slicing.

In Section 2 we begin by reviewing the syntax of Imp, giving illustrative examples of slicing, and then reviewing the theory of slicing using the Galois connection framework, including the properties of minimality and consistency. In Section 3 we introduce an instrumented, tracing semantics for Imp and present the forward and backward slicing algorithms. We formalise all of the theory from Section 3 in Coq and prove their duality. Section 4 highlights key elements of our Coq development, with full code available online [19]. Section 5 provides pointers to other related work.

2 Overview

2.1 Imp slicing by example

For the purpose of our analysis we use a minimal imperative programming language Imp used in some textbooks on programming languages, e.g. [13, 16, 22]111In the literature Imp is also referred to as WHILE.. Imp contains arithmetic and logical expressions, mutable state (a list of mappings from variable names to numeric values) and a small core of imperative commands: empty instruction (skip), variable assignments, instruction sequencing, conditional if instructions, and while loops. An Imp program is a series of commands combined using a sequencing operator. Imp lacks more advanced features, such as functions or pointers.

Figure 2 shows Imp syntax. We use letter $n$ to denote natural number constants and $x$ to denote program variables. In this presentation we have omitted subtraction ($-$) and multiplication ($\cdot$) from the list of arithmetic operators, and less-or-equal comparison ($\leq$) from the list of boolean operators. All these operators are present in our Coq development and we omit them here only to make the presentation in the paper more compact. Otherwise the treatment of subtraction and multiplication is analogous to the treatment of addition, and treatment of $\leq$ is analogous to $=$.

Dynamic slicing is a program simplification technique that determines which parts of the source code contributed to a particular program output. For example, a programmer might write this simple program in Imp:

if (y = 1) then { y := x + 1 } else { y := y + 1 } ; z := z + 1

and after running it with an input state $[\texttt{x}\mapsto 1,\texttt{y}\mapsto 0,\texttt{z}\mapsto 2]$ might (wrongly) expect to obtain output state $[\texttt{x}\mapsto 1,\texttt{y}\mapsto 2,\texttt{z}\mapsto 3]$. However, after running the program the actual output state will be $[\texttt{x}\mapsto 1,\texttt{y}\mapsto 1,\texttt{z}\mapsto 3]$ with value of y differing from the expectation.

We can use dynamic slicing to debug this program by asking for an explanation which parts of the source code and the initial input state contributed to incorrect output value of y. We do this by formulating a slicing criterion, where we replace all values that we consider irrelevant in the output state (i.e. don’t need an explanation for them) with holes (denoted with $\Box$):

[TABLE]

and a slicing algorithm might produce a program slice:

if (y = 1) then { $\Box$ } else { y := y + 1 } ; $\Box$

with a sliced input state $[\texttt{x}\mapsto\Box,\texttt{y}\mapsto 0,\texttt{z}\mapsto\Box]$. This result indicates which parts of the original source code and input state could be ignored when looking for a fault (indicated by replacing them with holes), and which ones were relevant in producing the output indicated in the slicing criterion. The result of slicing narrows down the amount of code a programmer has to inspect to locate a bug. Here we can see that only the input variable y was relevant in producing the result; x and z are replaced with a $\Box$ in the input state, indicating their irrelevance. We can also see that the first branch of the conditional was not taken (unexpectedly!) and that in the second branch y was incremented to become $1$. With irrelevant parts of the program hidden away it is now easier to spot that the problem comes from a mistake in the initial state. The initial value of y should be changed to $1$ so that the first branch of the conditional is taken and then y obtains an output value of $2$ as expected.

Consider the same example, but a different output slicing criterion $[\texttt{x}\mapsto\Box,\texttt{y}\mapsto\Box,\texttt{z}\mapsto 3]$. In this case, a correctly sliced program is as follows:

$\Box$ ; z := z + 1

with the corresponding sliced input $[\texttt{x}\mapsto\Box,\texttt{y}\mapsto\Box,\texttt{z}\mapsto 2]$, illustrating that the entire first conditional statement is irrelevant. However, while the conclusion seems intuitively obvious, actually calculating this correctly takes some work: we need to ensure that none of the assignments inside the taken conditional branch affected z, and conclude from this that the value of the conditional test y = 1 is also irrelevant to the final value of z.

2.2 A Galois connection approach to program slicing

Example in Section 2.1 relies on an intuitive feel of how backward slicing should behave. We now address the question of how to make that intuition precise and show that slicing using the Galois connection framework introduced by Perera et al. [15] offers an answer.

Consider these two extreme cases of backward slicing behaviour:

for any slicing criterion backward slicing always returns a full program with no holes inserted; 2. 2.

for any slicing criterion backward slicing always returns a $\Box$, i.e. it discards all the program code.

Neither of these two specifications is practically useful since they don’t fulfil our intuitive expectation of “discarding program fragments irrelevant to producing a given fragment of program output”. The first specification does not discard anything, bringing us no closer to understanding which code fragments are irrelevant. The second specification discards everything, including the code necessary to produce the output we want to understand. We thus want a backward slicing algorithm to have two properties:

• •

consistency: backward slicing retains code required to produce output we are interested in.

• •

minimality: backward slicing produces the smallest partial program and partial input state that suffice to achieve consistency.

Our first specification above does not have the minimality property; the second one does not have the consistency property. To achieve these properties we turn to order and lattice theory.

We begin with defining partial Imp programs (Figure 3) by extending Imp syntax presented in Figure 2 with holes (denoted using $\Box$ in the semantic rules). A hole can appear in place of any arithmetic expression, boolean expression, or command. In the same way we allow values stored inside a state to be mapped to holes. For example:

[TABLE]

is a partial state that maps variable x to $1$ and variable y to a hole. We also introduce operation $\varnothing_{\mu}$ that takes a state $\mu$ and creates a partial state with the same domain as $\mu$ but all variables mapped to $\Box$. For example if $\mu=[\texttt{x}\mapsto 1,\texttt{y}\mapsto 2]$ then $\varnothing_{\mu}=[\texttt{x}\mapsto\Box,\texttt{y}\mapsto\Box]$. A partial state that maps all its variables to holes is referred to as an empty partial state.

Having extended Imp syntax with holes, we define partial ordering relations on partial programs and partial states that consider holes to be syntactically smaller than any other subexpression. Figure 4 shows the partial ordering relation for arithmetic expressions. Definitions for ordering of partial boolean expressions and partial commands are analogous. Ordering for partial states is defined element-wise, thus requiring that two states in the ordering relation have identical domains, i.e. store the same variables in the same order.

For every Imp program $p$, a set of all partial programs smaller than $p$ forms a complete finite lattice, written ${\downarrow}p$ with $p$ being the top and $\Box$ the bottom element of this lattice. Partial states, arithmetic expressions, and boolean expressions form lattices in the same way. Moreover, a pair of lattices forms a (product) lattice, with the ordering relation defined component-wise:

[TABLE]

Figure 5 shows definition of the join (least upper bound, $\sqcup$) operation for arithmetic expressions. Definitions for boolean expressions and imperative commands are analogous. A join exists for every two elements from a complete lattice formed by a program $p$ or state $\mu$ [6, Theorem 2.31].

Assume we have a program $p$ paired with an input state $\mu$ that evaluates to an output state $\mu^{\prime}$. We can now formulate slicing as a pair of functions between lattices:

• •

forward slicing: Forward slicing can be thought of as evaluation of partial programs. A function $\mathsf{fwd}_{(p,\mu)}$ takes as its input a partial program and a partial state from a lattice formed by pairing a program $p$ and state $\mu$. $\mathsf{fwd}_{(p,\mu)}$ outputs a partial state belonging to a lattice formed by $\mu^{\prime}$. The input to the forward slicing function is referred to as a forward slicing criterion and output as a forward slice.

• •

backward slicing: Backward slicing can be thought of as “rewinding” a program’s execution. A function $\mathsf{bwd}_{\mu^{\prime}}$ takes as its input a partial state from the lattice formed by the output state $\mu^{\prime}$. $\mathsf{bwd}_{\mu^{\prime}}$ outputs a pair consisting of a partial program and a partial state, both belonging to a lattice formed by program $p$ and state $\mu$. Input to a backward slicing function is referred to as a backward slicing criterion and output as a backward slice.

A key point above (discussed in detail elsewhere [17]) is that for imperative programs, both $\mathsf{fwd}_{(p,\mu)}$ and $\mathsf{bwd}_{\mu^{\prime}}$ depend not only on $p,\mu,\mu^{\prime}$ but also on the particular execution path taken while evaluating $p$ on $\mu$. (In earlier work on slicing pure functional programs [15], traces are helpful for implementing slicing efficiently but not required for defining it.) We make this information explicit in Section 3 by introducing traces $T$ that capture the choices made during execution. We will define the slicing algorithms inductively as relations indexed by $T$, but in our Coq formalisation $\mathsf{fwd}^{T}_{(p,\mu)}$ and $\mathsf{bwd}^{T}_{\mu^{\prime}}$ are represented as dependently-typed functions where $T$ is a proof term witnessing an operational derivation.

A pair of forward and backward slicing functions is guaranteed to have both the minimality and consistency properties when they form a Galois connection [6, Lemmas 7.26 and 7.33].

Definition 1** (Galois connection).**

Given lattices $P$, $Q$ and two functions $f:P\rightarrow Q$, $g:Q\rightarrow P$, we say $f$ and $g$ form a Galois connection (written $f\dashv g$) when $\forall_{p\in P,q\in Q}f(p)\sqsubseteq_{Q}q\iff p\sqsubseteq_{P}g(q)$. We call $f$ a lower adjoint and $g$ an upper adjoint.

Importantly, for a given Galois connection $f\dashv g$, function $f$ uniquely determines $g$ and vice versa [6, Lemma 7.33]. This means that our choice of $\mathsf{fwd}$ (i.e. definition of how to evaluate partial programs on partial inputs) uniquely determines the backward slicing function $\mathsf{bwd}$ that will be minimal and consistent with respect to $\mathsf{fwd}$, provided we can show that $\mathsf{fwd}$ and $\mathsf{bwd}$ form a Galois connection. There are many strategies to show that two functions $f:P\rightarrow Q$ and $g:Q\rightarrow P$ form a Galois connection, or to show that $f$ or $g$ in isolation has an upper or respectively lower adjoint. One attractive approach is to show that $f$ preserves least upper bounds, or dually that $g$ preserves greatest lower bounds (in either case, monotonicity follows as well). This approach is indeed attractive because it allows us to analyse just one of $f$ or $g$ and know that its dual adjoint exists, without even having to write it down. Indeed, in previous studies of Galois slicing [15, 17], this characterisation was the one used: $\mathsf{fwd}$ was shown to preserve greatest lower bounds to establish the existence of its lower adjoint $\mathsf{bwd}$, and then efficient versions of $\mathsf{bwd}$ were defined and proved correct.

For our constructive formalisation, however, we really want to give computable definitions for both $\mathsf{fwd}$ and $\mathsf{bwd}$ and prove they form a Galois connection, so while preservation of greatest lower bounds by $\mathsf{fwd}$ is a useful design constraint, proving it does not really save us any work. Instead, we will use the following equivalent characterisation of Galois connections [6, Lemma 7.26]:

$f$ and $g$ are monotone 2. 2.

deflation property holds:

[TABLE] 3. 3.

inflation property holds:

[TABLE]

We use this approach in our Coq mechanisation. We will first prove a general theorem that any pair of functions that fulfils properties (1)–(3) above forms a Galois connection. We will then define forward and backward slicing functions for Imp programs and prove that they are monotone, deflationary, and inflationary. Once this is done we will instantiate the general theorem with our specific definitions of forward and backward slicing to arrive at the proof that our slicing functions form a Galois connection. This is the crucial correctness property that we aim to prove. We also prove that existence of a Galois connection between forward and backward slicing functions implies consistency and minimality properties. Note that consistency is equivalent to the inflation property.

3 Dynamic program slicing

3.1 Tracing semantics

Following previous work [15, 17], we employ a tracing semantics to define the slicing algorithms. Since dynamic slicing takes account of the actual execution path followed by a run of a program, we represent the execution path taken using an explicit trace data structure. Traces are then traversed as part of both the forward and backward slicing algorithms. That is, unlike tracing evaluation, forward and backward slicing follow the structure of traces, rather than the program. Note that we are not really inventing anything new here: in our formalisation, the trace is simply a proof term witnessing the derivability of the operational semantics judgement. The syntax of traces is shown in Figure 6. The structure of traces follows the structure of language syntax with the following exceptions:

• •

the expression trace $x(v_{a})$ records both the variable name $x$ and a value $v_{a}$ that was read from program state $\mu$;

• •

for conditional instructions, traces record which branch was actually taken. When the if condition evaluates to true we store traces of evaluating the condition and the then branch; if it evaluates to false we store traces of evaluating the condition and the else branch.

• •

for while loops, if the condition evaluates to false (i.e. loop body does not execute) we record only a trace for the condition. If the condition evaluates to true we record traces for the condition ($T_{b}$), a single execution of the loop body ($T_{c}$) and the remaining iterations of the loop ($T_{w}$).

Figures 7–9 show evaluation rules for arithmetic expressions, boolean expressions, and imperative commands, respectively222We overload the $\Rightarrow$ notation to mean one of three evaluation relations. It is always clear from the arguments which relation we are referring to.. Traces are written in grey colour and separated with a double colon ($::$) from the evaluation result. Arithmetic expressions evaluate to numbers (denoted $v_{a}$). Boolean expressions evaluate to either true or false (jointly denoted as $v_{b}$). Operators with N or B subscripts should be evaluated as mathematical and logical operators respectively to arrive at an actual value; this is to distinguish them from the language syntax. Commands evaluate by side-effecting on the input state, producing a new state as output (Figure 9). Only arithmetic values can be assigned to variables and stored inside a state. Assignments to variables absent from the program state are treated as no-ops. This means all variables that we want to write and read must be included (initialised) in the initial program state. We explain reasons behind this decision later in Section 4.3.

3.2 Forward slicing

In this and the next section we present concrete definitions of forward and backward slicing for Imp programs. Readers may prefer to skip ahead to Section 3.4 for an extended example of these systems at work first. Our slicing algorithms are based on the ideas first presented in [17]. Presentation in Section 2.2 views the slicing algorithms as computable functions and we will implement them in code as such. However for the purpose of writing down the formal definitions of our algorithms we will use a relational notation. It is more concise and allows easier comparisons with previous work.

Figures 10–12 present forward slicing rules for the Imp language333We again overload $\nearrow$ and $\searrow$ arrows in the notation to denote one of three forward/backward slicing relations. This is important in the rules for boolean slicing, whose premises refer to the slicing relation for arithmetic expressions, and command slicing, whose premises refer to slicing relation for boolean expressions.. As mentioned in Section 2.2, forward slicing can be thought of as evaluation of partial programs. Thus the forward slicing relations $\nearrow$ take a partial program, a partial state, and an execution trace as an input and return a partial value, either a partial number (for partial arithmetic expressions), a partial boolean (for partial logical expressions) or a partial state (for partial commands). For example, we can read {\color[rgb]{0.5,0.5,0.5}T::\ }\mu,c\nearrow\mu^{\prime} as “Given trace $T$, in partial environment $\mu$ the partial command $c$ forward slices to partial output $\mu^{\prime}$.”

A general principle in the forward slicing rules for arithmetic expressions (Figure 10) and logical expressions (Figure 11) is that “holes propagate”. This means that whenever $\Box$ appears as an argument of an operator, application of that operator forward slices to a $\Box$. For example, $1+\Box$ forward slices to a $\Box$ and so does $\neg\Box$. In other words, if an arithmetic or logical expression contains at least one hole it will reduce to a $\Box$; if it contains no holes it will reduce to a proper value. This is not the case for commands though. For example, command $\texttt{if}\;\texttt{true}\;\texttt{then}\;1\;\texttt{else}\;\Box$ forward slices to $1$, even though it contains a hole in the (not taken) else branch.

A rule worth attention is one for forward slicing of variable reads:

[TABLE]

It is important here that we read the return value from $\mu$ and not $v_{a}$ recorded in a trace. This is because $\mu$ is a partial state and also part of a forward slicing criterion. It might be that $\mu$ maps $x$ to $\Box$, in which case we must forward slice to $\Box$ and not to $v_{a}$. Otherwise minimality would not hold.

Forward slicing rules for arithmetic and logical expressions both have a universal rule for forward slicing of holes that applies regardless of what the exact trace value is:

[TABLE]

There is no such rule for forward slicing of commands (Figure 12). There we have separate rules for forward slicing of holes for each possible trace. This is due to the side-effecting nature of commands, which can mutate the state through variable assignments. Consider this rule for forward slicing of assignments w.r.t. a $\Box$ as a slicing criterion444When some partial value $v$ is used as a slicing criterion we say that we “slice w.r.t. $v$”.:

[TABLE]

When forward slicing an assignment w.r.t. a $\Box$ we need to erase (i.e. change to a $\Box$) variable $x$ in the state $\mu$, which follows the principle of “propagating holes”. Here having a trace is crucial to know which variable was actually assigned during the execution. Rules for forward slicing of other commands w.r.t. a $\Box$ traverse the trace recursively to make sure that all variable assignments within a trace are reached. For example:

[TABLE]

In this rule, trace $T_{1}$ is traversed recursively to arrive at a state $\mu^{\prime}$ that is then returned as the final product of the rule. Notice how trace $T_{b}$ is not traversed. This is because boolean expressions (and arithmetic ones as well) do not have side effects on the state and so there is no need to traverse them.

The problem of traversing the trace recursively to handle side-effects to the state can be approached differently. Authors of [17] have formulated a single rule, which we could adapt to our setting like this:

[TABLE]

In this rule $\mathsf{writes}(T)$ means “all state locations written to inside trace $T$” and $\mu\triangleleft\mathcal{L}$ means erasing (i.e. mapping to a $\Box$) all locations in $\mu$ that are mentioned in $\mathcal{L}$. Semantically this is equivalent to our rules – both approaches achieve the same effect. However, we have found having separate rules easier to formalise in a proof assistant.

3.3 Backward slicing

Backward slicing rules are given in Figures 13–15. These judgements should be read left-to-right, for example, {\color[rgb]{0.5,0.5,0.5}T::\ }\mu\searrow\mu^{\prime},c should be read as “Given trace $T$ and partial output state $\mu$, backward slicing yields partial input $\mu^{\prime}$ and partial command $c$.” Their intent is to reconstruct the smallest program code and initial state that suffice to produce, after forward slicing, a result that is at least as large as the backward slicing criterion. To this end, backward slicing crucially relies on execution traces as part of input, since slicing effectively runs a program backwards (from final result to source code).

Figures 13 and 14 share a universal rule for backward slicing w.r.t. a hole.

[TABLE]

This rule means that to obtain an empty result it always suffices to have an empty state and no program code. This rule always applies preferentially over other rules, which means that whenever a value, such as $v_{a}$ or $v_{b}$, appears as a backward slicing criterion we know it is not a $\Box$. Similarly, Figure 15 has a rule:

[TABLE]

It means that backward slicing w.r.t. a state with an empty domain (i.e. containing no variables) returns an empty partial state and an empty program. Of course having a program operating over a state with no variables would be completely useless – since a state cannot be extended with new variables during execution we wouldn’t observe any effects of such a program. However, in the Coq formalisation, it is necessary to handle this case because otherwise Coq will not accept that the definition of backward slicing is a total function.

In the rule for backward slicing of variable reads (third rule in Figure 13) it might seem that $v_{a}$ stored inside a trace is redundant because we know what $v_{a}$ is from the slicing criterion. This is a way of showing that variables can only be sliced w.r.t. values they have evaluated to during execution. So for example if $x$ evaluated to $17$ it is not valid to backward slice it w.r.t. $42$.

The rule for backward slicing of addition in Figure 13 might be a bit surprising. Each of the subexpressions is sliced w.r.t. a value that this expression has evaluated to ($v_{1}$, $v_{2}$), and not w.r.t. $v_{a}$. It might seem we are getting $v_{1}$ and $v_{2}$ out of thin air, since they are not directly recorded in a trace. Note however that knowing $T_{1}$ and $T_{2}$ allows to recover $v_{1}$ and $v_{2}$ at the expense of additional computations. In the actual implementation we perform induction on the structure of evaluation derivations, which record values of $v_{1}$ and $v_{2}$, thus allowing us to avoid extra computations. We show $v_{1}$ and $v_{2}$ in our rules but avoid showing the evaluation relation as part of slicing notation. This is elaborated further in Section 4.4.

Recursive backward slicing rules also rely crucially on the join ($\sqcup$) operation, which combines smaller slices from slicing subexpressions into one slice for the whole expression.

There are two separate rules for backward slicing of variable assignments (rules 3 and 4 in Figure 15). If a variable is mapped to a $\Box$ it means it is irrelevant. We therefore maintain mapping to a $\Box$ and do not reconstruct variable assignment instructions. If a variable is relevant though, i.e. it is mapped to a concrete value in a slicing criterion, we reconstruct the assignment instruction together with an arithmetic expression in the RHS. We also join state $\mu_{a}$ required to evaluate the RHS with $\mu[\texttt{x}\mapsto\Box]$. It is crucial that we erase $x$ in $\mu$ prior to joining. Firstly, if x is assigned, its value becomes irrelevant prior to the assignment, unless x is read during evaluation of the RHS (e.g. we are slicing an assignment x := x + 1). In this case x will be included in $\mu_{a}$ but its value can be different than the one in $\mu$. It is thus necessary to erase x in $\mu$ to make a join operation possible.

At this point, it may be helpful to review the forward rules for assignment and compare with the backward rules, illustrated via a small example. Suppose we have an assignment z := x + y, initially evaluated on $[\texttt{w}\mapsto 0,\texttt{x}\mapsto 1,\texttt{y}\mapsto 2,\texttt{z}\mapsto 42]$, and yielding result state $[\texttt{w}\mapsto 0,\texttt{x}\mapsto 1,\texttt{y}\mapsto 2,\texttt{z}\mapsto 3]$. The induced lattice of minimal inputs and maximal outputs consists of the following pairs:

[TABLE]

where $\texttt{v}\in\{\Box,0\}$ so that each line above abbreviates two concrete relationships; the lattice has the shape of a cube. Because $w$ is not read or written by z := x + y, it is preserved if present in the forward direction or if required in the backward direction. Because z is written but not read, its initial value is always irrelevant. To obtain the backward slice of any other partial output, such as $[\texttt{w}\mapsto\Box,\texttt{x}\mapsto 1,\texttt{y}\mapsto\Box,\texttt{z}\mapsto 3]$, find the smallest maximal partial output containing it, and take its backward slice, e.g. $[\texttt{w}\mapsto\Box,\texttt{x}\mapsto 1,\texttt{y}\mapsto 1,\texttt{z}\mapsto\Box]$.

In the backward slicing rules for if instructions, we only reconstruct a branch of the conditional that was actually taken during execution, leaving a second branch as a $\Box$. Importantly in these rules state $\mu_{b}$ is a minimal state sufficient for an if condition to evaluate to a true or false value. That state is joined with state $\mu^{\prime}$, which is a state sufficient to evaluate the reconstructed branch of an if.

Rules for while slicing follow a similar approach. It might seem that the second rule for slicing while${}_{\textsf{true}}$ is redundant because it is a special case of the third while${}_{\textsf{true}}$ rule if we allowed $c_{w}=\Box$. Indeed, that is the case on paper. However, for the purpose of a mechanised formalisation we require that these two rules are separate. This shows that formalising systems designed on paper can indeed be tricky and require modifications tailored to solve mechanisation-specific issues.

Readers might have noticed that whenever a backward slicing rule from Figure 15 returns $\Box$ as an output program, the state returned by the rule will be identical to the input state. One could then argue that we should reflect this in our rules by explicitly denoting that input and output states are the same, e.g.

[TABLE]

While it is true that in such a case states will be equal, this approach would not be directly reflected in the implementation, where slicing is implemented as a function and a result is always assigned to a new variable. However, it would be possible to prove a lemma about equality of input and output states for $\Box$ output programs, should we need this fact.

3.4 An Extended Example of Backward Slicing

We now turn to an extended example that combines all the programming constructs of Imp555This example is adapted from [9].: assignments, sequencing, conditionals, and loops. Figure 16 shows a program that divides integer a by b, and produces a quotient q, remainder r, and result res that is set to $1$ if b divides a and to [math] otherwise.

To test whether $2$ divides $4$ we set $\texttt{a}\mapsto 4$, $\texttt{b}\mapsto 2$ in the input state. The remaining variables q, r and res are initialised to [math] (Figure 16(a)). The while loop body is executed twice; the loop condition is evaluated three times. Once the loop has stopped, variable q is set to $2$ and variable r to [math]. Since the if condition is false we execute the else branch and set res to $1$. Figure 17 shows the execution trace.

We now want to obtain an explanation of res. We form a slicing criterion by setting $\texttt{res}\mapsto 1$ (this is the value at the end of execution); all other variables are set to $\Box$.

We begin by reconstructing the if conditional. We apply the second rule for $\texttt{if}_{\textsf{false}}$ slicing (Figure 16(b)). This is because $c_{2}$, i.e. the body of this branch, backward slices to an assignment res := 1, and not to a $\Box$ (in which case the first rule for $\texttt{if}_{\textsf{false}}$ slicing would apply). Assignment in the else branch is reconstructed by applying the second rule for assignment slicing. Since the value assigned to res is a constant it does not require presence of any variables in the state. Therefore state $\mu_{a}$ is empty. Moreover, variable res is erased in state $\mu$; joining of $\mu_{a}$ and $\mu[\texttt{res}\mapsto\Box]$ results in an empty state, which indicates that the code inside the else branch does not rely on the program state. However, to reconstruct the condition of the if we need a state $\mu_{b}$ that contains variable r. From the trace we read that $\texttt{r}\mapsto 0$, and so after reconstructing the conditional we have a state where $\texttt{r}\mapsto 0$ and all other variables, including res, map to $\Box$.

We now apply the third rule for sequence slicing and proceed with reconstruction of the while loop. First we apply a trivial $\texttt{while}_{\textsf{false}}$ rule. The rule basically says that there is no need to reconstruct a while loop that does not execute – it might as well not be in a program. Since the final iteration of the while loop was reconstructed as a $\Box$, we reconstruct the second iteration using the second $\texttt{while}_{\textsf{\small{true}}}$ backward slicing rule, i.e. the one where we have {\color[rgb]{0.5,0.5,0.5}T_{w}::\ }\mu\searrow\mu_{w},\Box as the first premise. We begin reconstruction of the body with the second assignment $\texttt{r}:=\texttt{r}(2)-\texttt{b}(2)$. Recall that the current state assigns [math] to r. The RHS is reconstructed using the second rule for backward slicing of assignments we have already applied when reconstructing else branch of the conditional. An important difference here is that r appears both in the LHS and RHS. Reconstruction of RHS yields a state where $\texttt{r}\mapsto 2$ and $\texttt{b}\mapsto 2$ (both values read from a trace), whereas the current state contains $\texttt{r}\mapsto 0$. Here it is crucial that we erase r in the current state before joining. We apply third rule of sequence slicing and proceed to reconstruct the assignment to q using the first rule for assignment slicing (since $\texttt{q}\mapsto\Box$ in the slicing criterion). This reconstructs the assignment as a $\Box$. We then reconstruct the first iteration of the loop using the third $\texttt{while}_{\textsf{\small{true}}}$ slicing rule, since it is the case that $c_{w}\neq\Box$. Assignments inside the first iteration are reconstructed following the same logic as in the second iteration, yielding a state where $\texttt{r}\mapsto 4$, $\texttt{b}\mapsto 2$, and other variables map to $\Box$.

Finally, we reconstruct the initial assignment r := a. Since r is present in the slicing criterion, we yet again apply the second rule for assignment slicing, arriving at a partial input state $[\texttt{q}\mapsto 0,\texttt{r}\mapsto 0,\texttt{res}\mapsto 0,\texttt{a}\mapsto 4,\texttt{b}\mapsto 2]$ and a partial program shown in Figure 16(b).

4 Formalisation

In the previous sections we defined the syntax and semantics of the Imp language, and provided definitions of slicing in a Galois connection framework. We have implemented all these definitions in the Coq proof assistant [20] and proved their correctness as formal theorems. The following subsections outline the structure of our Coq development. We provide references to the source code by providing the name of file and theorem or definition as (filename.v: theorem_name, definition_name). We will use * in abbreviations like *_monotone to point to several functions ending with _monotone suffix. The whole formalisation is around 5.2k lines of Coq code (not counting the comments). Full code is available online [19].

4.1 Lattices and Galois connections

Our formalisation is built around a core set of definitions and theorems about lattices and Galois connections. Most importantly we define:

• •

that a relation that is reflexive, antisymmetric and transitive is a partial order (Lattice.v: order). When we implement concrete definitions of ordering relations we require a proof that these implementations indeed have these three properties, e.g. (ImpPartial.v: order_aexpPO).

• •

what it means for a function $f:P\to Q$ to be monotone (Lattice.v: monotone):

[TABLE]

• •

consistency properties as given in Section 2.2 (Lattice.v: inflation, def-lation).

• •

a Galois connection of two functions between lattices $P$ and $Q$ (see Definition 1 in Section 2.2) (Lattice.v: galoisConnection).

We then prove that:

• •

existence of a Galois connection between two functions implies their consistency and minimality (Lattice.v: gc_implies_consistency, gc_implies_minimality).

• •

two monotone functions with deflation and inflation properties form a Galois connection (Lattice.v: cons_mono__gc).

Throughout the formalisation we operate on elements inside lattices of partial expressions (${\downarrow}a,{\downarrow}b$, commands (${\downarrow}c$) or states (${\downarrow}\mu$). We represent values in a lattice with an inductive data type prefix666Name comes from a term “prefix set” introduced in [17] to refer to a set of all partial values smaller than a given value. So a prefix set of a top element of a lattice denotes a set of all elements in that (complete) lattice. (PrefixSets.v: prefix) indexed by the top element of the lattice and the ordering relation777In order to make the code snippets in the paper easier to read we omit the ordering relation when indexing prefix.. Values of prefix data type store an element from a lattice together with the evidence that it is in the ordering relation with the top element. Similarly we define an inductive data type prefixO (PrefixSets.v: prefixO) for representing ordering of two elements from the same lattice. This data type stores the said two elements together with proofs that one is smaller than another and that both are smaller than the top element of a lattice.

4.2 Imp syntax and semantics

All definitions given in Figures 2–5 are directly implemented in our Coq formalisation.

Syntax trees for Imp (Figure 2), traces (Figure 6) and partial Imp (Figure 3) are defined as ordinary inductive data types in (Imp.v: aexp, bexp, cmd), (Imp.v: aexpT, bexpT, cmdT) and (ImpPartial.v: aexpP, bexpP, cmdP), respectively. We also define functions to convert Imp expressions to partial Imp expressions by rewriting from normal syntax tree to a partial one (ImpPartial.v: aexpPartialize, bexpPartialize, cmdPartialize).

Evaluation relations for Imp (Figures 7–9) and ordering relations for partial Imp (Figure 4) are defined as inductive data types with constructors indexed by elements in the relation (Imp.v: aevalR, bevalR, cevalR and ImpPartial.v: aexpPO, bexpPO, comPO), respectively. For each ordering relation we construct a proof of its reflexivity, transitivity, and antisymmetry, which together proves that a given relation is a partial order (ImpPartial.v: order_aexpPO, order_bexpPO, order_comPO).

Join operations (Figure 5) are implemented as functions (ImpPartial.v: aexpLUB, bexpLUB, comLUB). Their implementation is particularly tricky. Coq requires that all functions are total. We know that for two elements from the same lattice a join always exists, and so a join function is a total one. However, we must guarantee that a join function only takes as arguments elements from the same lattice. To this end a function takes three arguments: top element $e$ of a lattice and two prefix values $e_{1}$, $e_{2}$ indexed by the top element $e$. So for example if $e$ is a variable name $x$, we know that each of $e_{1}$ and $e_{2}$ is either also a variable name $x$ or a $\Box$. However, Coq does not have a built-in dependent pattern match and this leads to complications. In our example above, even if we know that $e$ is a variable name $x$ we still have to consider cases for $e_{1}$ and $e_{2}$ being a constant or an arithmetic operator. These cases are of course impossible, but it is the programmer’s responsibility to dismiss them explicitly. This causes further complications when we prove lemmas about properties of join, e.g.:

[TABLE]

This proof is done by induction on the top element of a lattice, where $e$, $e_{1}$, and $e_{2}$ are all smaller than that element. The top element limits the possible values of $e$, $e_{1}$, and $e_{2}$ but we still have to consider the impossible cases and dismiss them explicitly.

4.3 Program state

Imp programs operate by side-effecting on a program state. Handling of the state was one of the most tedious parts of the formalisation.

State is defined as a data type isomorphic to an association list that maps variables to natural number values (ImpState.v: state). Partial state is defined in the same way, except that it permits partial values, i.e. variables can be mapped to a hole or a numeric value (ImpState.v: stateP). We assume that no key appears more than once in a partial state. This is not enforced in the definition of stateP itself, but rather defined as a separate inductive predicate (ImpState.v: statePWellFormed) that is explicitly passed as an assumption to any theorem that needs it. We also have a statePartialize function that turns a state into a partial state. This only changes representation from one data type to another, with no change in the state contents.

For partial states we define an ordering relation as a component-wise ordering of partial values inside a state (ImpState.v: statePO). This assumes that domains of states in ordering relation are identical (same elements in the same order), which allows us to formulate lemmas such as:

[TABLE]

This lemma says that if a partial state $\mu$ is larger than an state with empty domain then $\mu$ itself must have an empty domain.

We also define a join operation on partial states, which operates element-wise on two partial states from the same lattice (ImpState.v: stateLUB).

As already mentioned in Section 3.1, the domain of the state is fixed throughout the execution. This means that updating a variable that does not exist in a state is a no-op, i.e. it returns the original state without any modifications. This behaviour is required to allow comparison of states before and after an update. Consider this lemma:

[TABLE]

It says that if a partial state $\mu_{1}$ is smaller than $\mu_{2}$ and the value stored in state $\mu_{2}$ under key $k$ is greater than $v_{1}$ then we can assign $v_{1}$ to key $k$ in $\mu_{1}$ and the ordering between states will be maintained. A corner-case for this theorem is when the key $k$ is absent from the states $\mu_{1}$ and $\mu_{2}$. Looking up a non-existing key in a partial state returns a $\Box$. If $k$ did not exist in $\mu_{2}$ (and thus $\mu_{1}$ as well) then $\mu_{2}(k)$ would return $\Box$ and so $v_{1}$ could only be a $\Box$ (per second assumption of the theorem). However, if we defined semantics of update to insert a non-existing key into the state, rather than be a no-op, the conclusion of the theorem would not hold because domain of $\mu_{1}[k\mapsto v_{1}]$ would contain $k$ and domain of $\mu_{2}$ would not, thus making it impossible to define the ordering between the two states.

The approach described above is one of several possible design choices. One alternative approach would be to require evidence that the key being updated exists in the state, making it impossible to attempt update of non-existent keys. We have experimented with this approach but found explicit handling of evidence that a key is present in a state very tedious and seriously complicating many of the proofs. In the end we decided for the approach outlined above, as it allowed us to prove all the required lemmas, with only some of them relying on an explicit assumption that a key is present in a state. An example of such a lemma is:

[TABLE]

which says that if we update key $k$ in a partial state $\mu$ with value $v$ and then immediately lookup $k$ in the updated state we will get back the $v$ value we just wrote to $\mu$. However, this statement only holds if $k$ is present in $\mu$. If it was absent the update would return $\mu$ without any changes and then lookup would return $\Box$, which makes the theorem statement false. Thus this theorem requires passing explicit evidence that $k\in\mathsf{dom}(\mu)$ in order for the conclusion to hold.

Formalising program state was a tedious task, requiring us to prove over sixty lemmas about the properties of operations on state, totalling over 800 lines of code.

4.4 Slicing functions

Slicing functions implement rules given in Figures 10–15. We have three separate forward slicing functions, one for arithmetic expressions, one for logical expressions and one for imperative commands (ImpSlicing.v: aexpFwd, bexpFwd, comFwd). Similarly for backward slicing (ImpSlicing.v: aexpBwd, bexpBwd, comBwd).

In Section 2.2 we said that forward and backward slicing functions operate between two lattices. If we have an input $p$ (an arithmetic or logical expression or a command) with initial state $\mu$ that evaluates to output $p^{\prime}$ (a number, a boolean, a state) and records a trace $T$ then $\mathsf{fwd}^{T}_{(p,\mu)}$ is a forward slicing function parametrized by $T$ that takes values from lattice generated by $(p,\mu)$ to values in lattice generated by $p^{\prime}$. Similarly $\mathsf{bwd}^{T}_{p^{\prime}}$ is a backward slicing function parametrized by $T$ that takes values from lattice generated by $p^{\prime}$ to values in lattice generated by $(p,\mu)$. Therefore our implementation of forward and backward slicing functions has to enforce that:

$(p,\mu)$ evaluates to $p^{\prime}$ and records trace $T$ 2. 2.

forward slicing function takes values from lattice generated by $(p,\mu)$ to lattice generated by $p^{\prime}$ 3. 3.

backward slicing function takes values from lattice generated by $p^{\prime}$ to lattice generated by $(p,\mu)$

To enforce the first condition we require that each slicing function is parametrized by inductive evidence that a given input $(p,\mu)$ evaluates to $p^{\prime}$ and records trace $T$. We then define input and output types of such slicing functions as belonging to relevant lattices, which is achieved using the prefix data type described in Section 4.1. This enforces the conditions above. For example, the type signature of the forward slicing function for arithmetic expressions looks like this:

Fixpoint aexpFwd {st : state} {a : aexp} {v : nat} {t : aexpT} (ev : t :: a, st \ v): (prefix a * prefix st) -> prefix v.

Here ev is evidence that arithmetic expression a with input state st evaluates to a natural number v and records an execution trace t. The t :: a, st \  v syntax is a notation for the evaluation relation. The first four arguments to aexpFwd are in curly braces, denoting they are implicit and can be inferred from the type of ev. The function then takes values from the lattice generated by (a, st) and returns values in the lattice generated by v.

In the body of a slicing function we first decompose the evaluation evidence with pattern matching. In each branch we implement logic corresponding to relevant slicing rules defined in Figures 10–15. Premises appearing in the rules are turned into recursive calls. If necessary, results of these calls are analysed to decide which rule should apply. For example, when backward slicing sequences we analyse whether the recursive calls return holes or expressions to decide which of the rules should apply.

The implementation of the slicing functions faces similar problems as the implementation of joins described in Section 4.2. When we pattern match on the evaluation evidence, in each branch we are restricted to concrete values of the expression being evaluated. For example, if the last step in the evaluation was an addition, then we know the slicing criterion is a partial expression from a lattice formed by expression $a_{1}+a_{2}$. Yet we have to consider the impossible cases, e.g. having an expression that is a constant, and dismiss them explicitly. Moreover, operating inside a lattice requires us not to simply return a result, but also provide a proof that this result is inside the required lattice. We rely on Coq’s refine tactic to construct the required proof terms. All of this makes the definitions of slicing functions very verbose. For example, forward slicing of arithmetic expressions requires over 80 lines of code with over 60 lines of additional boilerplate lemmas to dismiss the impossible cases.

For each slicing function we state and prove a theorem that it is monotone (ImpSlicing.v: *_monotone). For each pair of forward and backward slicing functions we state theorems that these pairs of functions have deflation and inflation properties (ImpSlicing.v: *_deflating, *_inflating), as defined in Section 2.2. Once these theorems are proven we create instances of a general theorem cons_mono__gc, described in Section 4.1, which proves that our definitions form a Galois connection and are thus a correctly defined pair of slicing functions. We also create instances of the gc_implies_minimality theorem, one instance for each slicing function. This provides us with a formalisation of all the correctness properties, proving our main result:

Theorem 1**.**

Suppose \mu_{1},c\Rightarrow{\color[rgb]{0.5,0.5,0.5}T::\ }\mu_{2}. Then there exist total, monotone functions $\mathsf{fwd}^{T}_{(c,\mu_{1})}:{\downarrow}c\times{\downarrow}\mu_{1}\to{\downarrow}\mu_{2}$ and $\mathsf{bwd}^{T}_{\mu_{2}}:{\downarrow}\mu_{2}\to{\downarrow}c\times{\downarrow}\mu_{1}$. Moreover, $\mathsf{bwd}^{T}_{\mu_{2}}\dashv\mathsf{fwd}^{T}_{(c,\mu_{1})}$ form a Galois connection and in particular satisfy the minimality, inflation (consistency), and deflation properties.

Here, the forward and backward slicing judgements are implemented as functions $\mathsf{fwd}^{T}_{(c,\mu_{1})}$ and $\mathsf{bwd}^{T}_{\mu_{2}}$.

5 Related and Future Work

During the past few decades a plethora of slicing algorithms has been presented in the literature. See [18] for a good, although now slightly out of date, survey. Most of these algorithms have been analysed in a formal setting of some sort using pen and paper. However, work on formalising slicing in a machine checked way has been scarce. One example of such a development is [14], which formalises dynamic slicing for $\pi$-calculus in Agda using a Galois connection framework identical to the one used in this paper. The high-level outline of the formalisation is thus similar to ours. However, details differ substantially, since [14] formalises a completely different slicing algorithm for concurrent processes using a different proof assistant. Another example of formalising slicing in a proof assistant is [3], where Coq is used to perform an a posteriori validation of a slice obtained using an unverified program slicer. This differs from our approach of verifying correctness of a slicing algorithm itself. We see our approach of verifying correctness of the whole algorithm as a significant improvement over the validation approach. In a more recent work Léchenet et al. [9] introduce a variant of static slicing known as relaxed slicing and use Coq to formalise the slicing algorithm. Their work is identical in spirit to ours and focuses on the Imp language888Authors of [9] use the name WHILE, but the language is the same. with an extra assert statement.

Galois connections have been investigated previously as a tool in the mathematics of program construction, for example by Backhouse [1] and more recently by Mu and Oliveira [12]. As discussed in Section 1, Galois connections capture a common pattern in which one first specifies a space of possible solutions to a problem, the “easy” part, via one adjoint, and defines the mapping from problem instances to optimal solutions, the “hard” part, as the Galois dual. In the case of slicing, we have used the goal of obtaining a verifiable Galois connection, along with intuition, to motivate choices in the design of the forward semantics, and it has turned out to be easier for our correctness proof to define both directions directly.

Mechanised proofs of correctness of calculational reasoning has been considered in the Algebra of Programming in Agda (AOPA) system [11], and subsequently extended to include derivation of greedy algorithms using Galois connections [5]. Another interesting, complementary approach to program comprehension is Gibbons’ program fission [7], in which the fusion law is applied “in reverse” to an optimized, existing program in order to attempt to discover a rationale for its behavior: for example by decomposing an optimized word-counting program into a “reforested” version that decomposes its behavior into “construct a list of all the words” and “take the length of the list”. We conjecture that the traces that seem to arise as a natural intermediate structure in program slicing might be viewed as an extreme example of fission.

An important line of work on slicing theory focuses on formalising different slicing algorithms within a unified theoretical framework of program projection [2]. Authors of that approach develop a precise definition of what it means that one form of slicing is weaker than another. However, our dynamic slicing algorithm does not fit the framework as presented in [2]. We believe that it should be possible to extend the program projection framework so that it can encompass slicing based on Galois connections but this is left as future work.

6 Summary

Program slicing is an important tool for aiding software development. It is useful when creating new programs as well as maintaining existing ones. In this paper we have developed and formalised an algorithm for dynamic slicing of imperative programs. Our work extends the line of research on slicing based on the Galois connection framework. In the presented approach slicing consists of two components: forward slicing, that allows to execute partial programs, and backward slicing, that allows to “rewind” program execution to explain the output.

Studying slicing in a formal setting ensures the reliability of this technique. We have formalised all of the theory presented in this paper using the Coq proof assistant. Most importantly, we have shown that our slicing algorithms form a Galois connection, and thus have the crucial properties of consistency and minimality. One interesting challenge in our mechanisation of the proofs was the need to modify some of the theoretical developments so that they are easier to formalise in a proof assistant – c.f. overlapping rules for backward slicing of while loops described in Section 3.3.

Our focus in this paper was on a simple programming language Imp. This work should be seen as a stepping stone towards more complicated formalisations of languages with features like (higher-order) functions, arrays, and pointers. Though previous work [17] has investigated slicing based on Galois connections for functional programs with imperative features, our experience formalising slicing for the much simpler Imp language suggests that formalising a full-scale language would be a considerable effort. We leave this as future work.

Acknowledgements

We gratefully acknowledge help received from Wilmer Ricciotti during our work on the Coq formalisation, and Jeremy Gibbons for comments on a draft. This work was supported by ERC Consolidator Grant Skye (grant number 682315).