This paper was converted on www.awesomepapers.org from LaTeX by an anonymous user.
Want to know more? Visit the Converter page.

Syndicate: Synergistic Synthesis of Ranking Function and Invariants for Termination Analysis

Yasmin Sarita University of Illinois Urbana-ChampaignUSA [email protected] ,  Avaljot Singh University of Illinois Urbana-ChampaignUSA [email protected] ,  Shaurya Gomber University of Illinois Urbana-ChampaignUSA [email protected] ,  Gagandeep Singh University of Illinois Urbana-Champaign and VMware ResearchUSA [email protected]  and  Mahesh Vishwanathan University of Illinois Urbana-ChampaignUSA [email protected]
Abstract.

Several techniques have been developed to prove the termination of programs. Finding ranking functions is one of the common approaches to do so. A ranking function must be bounded and must reduce at every iteration for all the reachable program states. Since the set of reachable states is often unknown, invariants serve as an over-approximation. Further, in the case of nested loops, the initial set of program states for the nested loop can be determined by the invariant of the outer loop. So, invariants play an important role in proving the validity of a ranking function in the absence of the exact reachable states. However, in the existing techniques, either the invariants are synthesized independently, or combined with ranking function synthesis into a single query, both of which are inefficient.

We observe that a guided search for invariants and ranking functions can have benefits in terms of the number of programs that can be proved to terminate and the time needed to identify a proof of termination. So, in this work, we develop Syndicate, a novel framework that synergistically guides the search for both the ranking function and an invariant that together constitute a proof of termination. Owing to our synergistic approach, Syndicate can not only prove the termination of more benchmarks but also achieves a reduction ranging from 17% to 70% in the average runtime as compared to existing state-of-the-art termination analysis tools. We also prove that Syndicate is relatively complete, i.e., if there exists a ranking function and an invariant in their respective templates that can be used to prove the termination of a program, then Syndicate will always find it if there exist complete procedures for the template-specific functions in our framework.

Termination, Program Analysis, Verification, Ranking functions, Invariants
††copyright: acmlicensed††journal: JACM††journalvolume: 37††journalnumber: 4††article: 111††publicationmonth: 8††copyright: none††ccs: Software and its engineering Formal software verification††ccs: Theory of computation Program verification

1. Introduction

Termination analysis is one of the most challenging components of program verification. Several techniques for automatically proving termination or non-termination have been explored in the past. These include using various reduction orders, finding recurrent sets, fixpoint logic solving, etc, within static or dynamic analyses or a combination of both (Giesl et al., 2017; Heizmann et al., 2014; Le et al., 2020; Unno et al., 2023). One of the most common techniques to prove the termination of programs and also the focus of this work is finding ranking functions. Ranking functions have the property that for all reachable states, they are bounded from below and decrease by at least a certain amount in each iteration. This poses a problem because computing the exact set of reachable states is undecidable. To overcome this, loop invariants are typically used as an over-approximation of the reachable states. So, to prove the termination of a program, there are two unknowns - the ranking function and the loop invariant. However, synthesizing both ranking functions and loop invariants together is challenging. Compared with classical property-guided synthesis (Welp and Kuehlmann, 2014; Bradley, 2011), we do not have direct access to the target property (a ranking function or an invariant). Instead, we only know constraints on the target properties, i.e., the ranking function must be bounded and must reduce on all reachable states, and the invariants must subsume the initial program states and must be inductive.

Some existing termination analysis techniques like (Giacobbe et al., 2022; Le et al., 2020) handle the above issue by synthesizing the invariants and ranking functions independently and work by either hard-coding some candidate invariants or outsourcing the invariant generation to an external solver. Due to this independence, these techniques frequently spend a significant amount of time in discovering invariants that are either not useful to prove termination or are stronger than necessary. Techniques like  (Cook et al., 2006) use their current set of ranking functions to guide a binary reachability analysis procedure. However, this procedure is done using an external temporal safety checker, so insights gained during one call to the safety checker cannot be used to guide the ranking function generation procedure or future calls to the safety checker. On the opposite side of the spectrum, methods such as (Unno et al., 2021) pose the synthesis of ranking functions and an over-approximation of the reachable states into a task of verifying the satisfiability of a formula in fixpoint logic. This tightly couples both tasks, making the search space for the combined query a significantly large product of their individual search spaces.

Synergy. We argue that for a given program with a single loop, although the search for ranking functions and the corresponding invariants must not be agnostic of each other, directly encoding them as a monolithic query can make each step of the search expensive. So, we propose that they should still be searched using separate subroutines, but both sub-routines must exchange key information with each other. Suppose the ranking function generated by the ranking function synthesizer is invalid. In that case, the generated counter-example can be used in one of these two ways: (1) if the counter-example is not a reachable program state, it can guide the invariant synthesizer toward a new invariant that excludes the counter-example, or (2) if the counter-example is reachable and we find that no possible invariant can exclude it, this search for a possible invariant will enable the discovery of new program states that are conclusively reachable. These states then guide the search for a new candidate ranking function. Since both the searches guide each other with the common goal of finding a valid termination argument, this synergy enables an efficient search for a ranking function and an invariant that is just strong-enough to prove termination. Synergistic search of ranking function and invariant synthesizers is computationally efficient, thus allowing the advantages of both sides of the spectrum while minimizing their drawbacks.

Multiple Loops. Proving the termination of programs with multiple loops (nested or sequential) adds another level to the problem’s difficulty. All the loops in the program must terminate, however, the search for ranking functions and corresponding invariants cannot be independent across different loops. For instance, in the case of nested loops, the invariant of the outer loop defines the over-approximation of the initial set of the inner loop. So, the precision of the outer invariant affects the inner loop’s invariant and ranking function. Conversely, the inner invariant describes the over-approximated transition relation of the outer loop’s body and thus affects the search for the outer loop’s invariant and ranking function. Also, as expected, it is inefficient to encode the search for all the invariants and the ranking functions as a single query because of the prohibitively large search space, and it may not even be needed in most cases. To address this problem, in addition to having synergy between the searches for a ranking function and invariant for one loop, we must also use the information from the invariant search in each loop to guide the searches for ranking functions and invariants of other loops in the program.

This Work. We introduce a new, general, framework called Syndicate, based on a synergistic synthesis of ranking functions and invariants for efficient termination analysis of complex programs containing arbitrarily nested loops, disjunctive conditionals, and non-linear statements. Syndicate is data-driven and synthesizes ranking functions from execution traces which makes it less dependent on the exact structure of the loop. It is parameterized by a set of possible invariants ℐ\mathcal{I} and a set of possible ranking functions ℱ\mathcal{F} and can be instantiated with different choices of these sets to obtain different termination analyses. For each loop, counter-examples from the invariant search guide the ranking function search, and counter-examples from the ranking function search guide the invariant search. Further, the invariant and ranking function searches for each loop are guided by the analyses of the other loops in the program. Under computability assumptions and assumptions on the structure of ℐ\mathcal{I} and ℱ\mathcal{F}, we guarantee completeness: for a given program PP, if there is a termination proof using the invariants in ℐ\mathcal{I} and ranking functions in ℱ\mathcal{F}, then Syndicate will find a ranking function f∈ℱf\in\mathcal{F} that is valid under an invariant 𝖨∈ℐ\mathsf{I}\in\mathcal{I} for every loop in PP.

Main Contributions:

  • •

    We provide a general recipe for the synergistic synthesis of invariants and ranking functions in the form of a framework called Syndicate, which can be instantiated with different templates for ranking functions and invariants. To do this, we introduce annotated programs with which we build the necessary formalism needed for synergistic search. Syndicate handles complex programs with arbitrarily nested and sequential loops, disjunctive conditionals, and non-linear statements.

  • •

    We show an additive upper bound on the number of iterations in terms of the depths of lattices of invariants and ranking functions, while also guaranteeing the soundness and relative completeness of Syndicate.

  • •

    We provide an implementation of Syndicate and evaluate it on challenging benchmarks (Beyer, 2020; Giesl et al., 2019; Giacobbe et al., 2022). Our results show that we outperform state-of-the-art termination analysis tools (Giacobbe et al., 2022; Giesl et al., 2017; Le et al., 2020; Heizmann et al., 2014) both in the number of benchmarks proved and in the average time. We also prove some benchmarks that none of these analysis tools can prove.

2. Overview

We aim to find a ranking function ff for a loop program 𝖫=while​(β)​ do ​𝖯1​ od\mathsf{L}=\texttt{while}(\beta)\texttt{ do }\mathsf{P}_{1}\texttt{ od} in some program 𝖯\mathsf{P}. We use ℛ\mathcal{R} to refer to the set of reachable program states at the beginning of the loop and ⟦𝖯1⟧\llbracket\mathsf{P}_{1}\rrbracket to refer to the relation that captures the semantics of the loop body 𝖯1\mathsf{P}_{1}. Note that 𝖯1\mathsf{P}_{1} can itself have loops. A function ff is a valid ranking function for the loop program 𝖫\mathsf{L} w.r.t ℛ,⟦𝖯1⟧\mathcal{R},\llbracket\mathsf{P}_{1}\rrbracket if it is bounded for all states in ℛ\mathcal{R} and reduces for all pairs of states in ⟦𝖯1⟧\llbracket\mathsf{P}_{1}\rrbracket.

  1. (1)

    Bounded: ∀s∈ℛ⋅f​(s)≥0\forall s\in\mathcal{R}\cdot f(s)\geq 0

  2. (2)

    Reducing: ∀(s,s′)∈𝖯1⋅f​(s)−f​(s′)≥1\forall(s,s^{\prime})\in\mathsf{P}_{1}\cdot f(s)-f(s^{\prime})\geq 1

Typically, ranking functions are only required to be bounded above some value (say θ\theta) and decrease by some minimum amount (say δ\delta). However, if a ranking function gg satisfying the more general properties exists, then a ranking function bounded by 0 and reducing by at least one exists. At each step of our algorithm, we maintain a state defined by a tuple ⟨t,𝖠𝖫⟩\langle t,\mathsf{A}_{\mathsf{L}}\rangle. t⊆S×St\subseteq S\times S is a set of pairs of states occurring at the start and end of the loop body, initially sampled by executing the program on random inputs. tt serves as an under-approximation of ⟦𝖯⟧1\llbracket\mathsf{P}\rrbracket_{1} such that 𝖽𝗈𝗆​(t)⊆ℛ\mathsf{dom}(t)\subseteq\mathcal{R}. The second part of the algorithm state, 𝖠𝖫\mathsf{A}_{\mathsf{L}}, stores the program as well as invariants associated with each loop in the program. These invariants can be used to define an over-approximation of the reachable states at each loop head. The loop body transition relation can also be over-approximated using the loop invariant 𝖨\mathsf{I} and the loop guard β\beta as 𝖨×(𝖨∩⟦¬β⟧)\mathsf{I}\times(\mathsf{I}\cap\llbracket\neg\beta\rrbracket). We define the structure, 𝖠𝖫=𝖨​@​while​(β)​ do ​𝖠1​ od\mathsf{A}_{\mathsf{L}}=\mathsf{I}\;@\;\texttt{while}(\beta)\texttt{ do }\mathsf{A}_{1}\texttt{ od}, as an annotated program, where each loop in the program is annotated by its invariant. Sematics of any program 𝖯\mathsf{P}, ⟦𝖯⟧\llbracket\mathsf{P}\rrbracket, can then be over-approximated using the invariants in the annotated program 𝖠\mathsf{A}. This over-approximation is denoted by ⟦𝖠⟧\llbracket\mathsf{A}\rrbracket. We define annotated programs formally in Section 4.

We present Syndicate which iteratively generates a candidate ranking function ff and then refines the state of the algorithm until the generated candidate is proven to be valid. We can generate a candidate ranking function by finding a function that satisfies the Bounded and Reducing properties on the states in tt since tt is an under-approximation of ⟦𝖯⟧1\llbracket\mathsf{P}\rrbracket_{1} and 𝖽𝗈𝗆​(t)⊆ℛ\mathsf{dom}(t)\subseteq\mathcal{R}.

(1) ∀(s,s′)∈t⋅(f​(s)−f​(s′)≥1)∧(f​(s)≥0)\forall(s,s^{\prime})\in t\cdot\big{(}f(s)-f(s^{\prime})\geq 1\big{)}\wedge\big{(}f(s)\geq 0\big{)}

We then check the validity of the ranking function using 𝖠𝖫\mathsf{A}_{\mathsf{L}}.

(2) ∀(s,s′)∈⟦𝖠𝖫⟧⋅(s∈⟦β⟧)⟹(f(s)−f(s′)≥1∧f(s)≥0)\forall(s,s^{\prime})\in\llbracket\mathsf{A}_{\mathsf{L}}\rrbracket\cdot(s\in\llbracket\beta\rrbracket)\implies(f(s)-f(s^{\prime})\geq 1\wedge f(s)\geq 0)

If we cannot prove the validity of the ranking function, we obtain a counter-example (p,p′)(p,p^{\prime}) on which either the Bounded or Reducing property is not satisfied. Using this counter-example, we refine the state of our algorithm. At this point, there can be two possibilities - (i) pp is not a reachable state, which implies that the invariant 𝖨\mathsf{I} is weak, or (ii) ff is invalid. We first try to refine the invariant to exclude the counterexample (p,p′)(p,p^{\prime}). This is further done in two steps which are explained later in this section. If we can refine the invariant, we update 𝖠𝖫\mathsf{A}_{\mathsf{L}} with a stronger invariant. If we cannot find an invariant that excludes (p,p′)(p,p^{\prime}), then (p,p′)(p,p^{\prime}) is added to the set tt. In either case, we have a refinement of the algorithm state that leads to a better approximation of the reachable states ℛ\mathcal{R}. The process continues until we find a ranking function and an invariant that constitute a valid proof of termination of 𝖫\mathsf{L}. While trying to refine the invariant, we may also encounter some reachable states {(q1,q1′),(q2,q2′),⋯}\{(q_{1},q^{\prime}_{1}),(q_{2},q^{\prime}_{2}),\cdots\} that are not already in tt. These are also added to tt during the refinement of the algorithm state. Note that the counter-example (p,p′)(p,p^{\prime}) guides the search for an invariant that can prove the current candidate ranking function, and the new reachable state pairs {(qi,qi′)}\{(q_{i},q_{i}^{\prime})\} guide the search for better candidate ranking functions in subsequent iterations of our algorithm.

Refer to caption
Figure 1. For a single loop, we maintain r,𝖨r,\mathsf{I} as canonical representations of t,𝖠𝖫t,\mathsf{A}_{\mathsf{L}} respectively. First, we use the set rr to generate a candidate ranking function and then use the invariant 𝖨\mathsf{I} to check the validity. If we get a counter-example pp, we try to refine the invariant 𝖨\mathsf{I} to exclude pp. If pp is not reachable, the invariant is refined successfully. Otherwise, we add pp and qq (reachable states discovered while trying to refine 𝖨\mathsf{I}) to the set rr.

In our algorithm we define ℐ\mathcal{I} to be the set of possible invariants we can use for a loop. Because of this, when we say a counter-example, ss, is reachable, we mean there is no valid invariant in ℐ\mathcal{I} that excludes ss. Similarly, we define ℱ\mathcal{F} to be the set of possible ranking functions and we only synthesize ranking functions from this set.

2.1. Syndicate Through an Example

⬇
1 y = n;
2 z = n+1;
3 while (m+y >= 0 &&
4 m <= n)
5 {
6 m = 2 * m + y;
7 y = z;
8 z = z + 1;
9 }\end{lstlisting}
10 \caption{Example terminating program}
11 \label{overview:code3}
12 \end{minipage}
13 \hspace{0.4cm}
14 \begin{minipage}{0.6\textwidth}
15 \scriptsize
16 \begin{align*}
17 \qquad&\rf(m’, y’, z’, n’) \\
18 &= \max\big(1-(m’+y’), 0\big) + \max(n’ - m’ + 1, 0) \\
19 &= \max\big(1-2m-y-z, 0\big) + \max(n-2m-y+1,0) \\
20 &= \max\big(1-2m-y-\fbox{\textbf{(y+1)}}, 0\big) + \max\big(n-m+1-(m+y),0\big) \\
21 &= \max(-2m-2y, 0) + \max\big(n-m+1-(m+y),0\big) \\
22 &= 0 +\max\big(n-m+1-(m+y),0\big) \\
23 &= \max\big(n-m+1-(m+y),0\big) \\
24 &\leq \rf(m, y, z, n) - 1
25 \end{align*}
26 \caption{Value of Ranking function at the end of one iteration}
27 \label{overview:rankingred2}
28 \end{minipage}
29\end{figure}
30
31\begin{table}
32 \centering
33 \scriptsize
34 \resizebox{0.8\textwidth}{!}{
35 \begin{tabular}{@{}lrrrr@{}}
36 \hline
37 &$r$ & $\invar$ & $\rf$ & $cex$ \\
38 \hline
39 1&$\{(1,2,3,4),(2,2,3,4)\}$ & $\true$ & $\max(n-m,0)$ & $(1,-1,2,4)$ \\
40 % \multirow{2}{*}{1}&$\{(1,2,3,4),$ & \multirow{2}{*}{$\true$} & \multirow{2}{*}{$\max(n-m,0)$} & \multirow{2}{*}{$(1,-1,2,4)$} \\
41 % &$(2,2,3,4)\}$ & & & \\
42 \hline
43 2&$\{(1,2,3,4),(2,2,3,4)\}$ & \textcolor{blue}{$y+1 \geq z$} & $\max(n-m,0)$ & $(1,-1,-1,1)$ \\
44 % \multirow{2}{*}{2}&$\{(1,2,3,4)$ & \multirow{2}{*}{$\textcolor{blue}{y+1\geq z}$} & \multirow{2}{*}{$\max(n-m,0)$} & \multirow{2}{*}{$(1,-1,-1,1)$} \\
45 % &$(2,2,3,4)\}$ & & & \\
46 \hline
47 \multirow{2}{*}{3}&$\{(1,2,3,4),(2,2,3,4),$ & \multirow{2}{*}{$\textcolor{blue}{(y+1\geq z) \wedge (y+1\leq z)}$} & \multirow{2}{*}{$\textcolor{blue}{\max(n-m+1,0)}$} & \multirow{2}{*}{$(1,-1,0,4)$} \\
48 &$\textcolor{blue}{(1,1,2,1)}\}$ & & & \\
49 \hline
50 \multirow{2}{*}{4}&$\{(1,2,3,4), (2,2,3,4), $ & \multirow{2}{*}{$(y\geq z-1) \wedge (y\leq z-1)$} & $\textcolor{blue}{\max(n-m+1,0) + }$ & \multirow{2}{*}{-} \\
51 &$(1,1,2,1),\textcolor{blue}{(1,-1,0,4)}\}$ & & $\textcolor{blue}{\max(1-m-y, 0)}$ & \\
52 \hline
53 \end{tabular}
54 }
55 \caption{Steps taken by \toolname to prove the termination for the program in Fig.~\ref{overview:code3}}
56 \label{tab:overview1}
57\end{table}
58
59% \begin{wrapfigure}{l}{0.5\linewidth}
60% \begin{lstlisting}[numbers=left,basicstyle=\ttfamily\footnotesize,backgroundcolor=\color{backcolour}]
61% y = n;
62% z = n+1;
63% while (m + y >= 0 && m <= n) {
64% m = 2 * m + y;
65% y = z;
66% z = z + 1;
67% }\end{lstlisting}
68% \caption{Example terminating program}
69% \label{overview:code3}
70% \end{wrapfigure}
71\noindent
72We show the working of \toolname on a terminating single-loop program in Fig.~\ref{overview:code3}.
73% \mvcom{Maybe you mean Program in Fig.~\ref{overview:code3}?}
74% (taken from the benchmarks used in Section~\ref{sec:evaluation} \sgcom{I remember me and Aval coming up with this to demonstrate the approach easily, is it fine to write that this is from the benchmarks}).
75In each iteration, $z$ increases by 1, and as $y$ is set to the previous iteration value of $z$, $y$ also increases by 1. For each iteration, $m+y\ge 0$ and $m\le n$ (from the loop guard). In each iteration, $m$ increases by $m + y$. There are two cases: (1) If $m + y > 0$ at the beginning of the first iteration, then $m$ will increase in every iteration and eventually be greater than $n$, and (2) If $m + y = 0$ at the beginning of the first iteration, $m$ stays constant for the first iteration, $y$ always increases (as noted above), which means that after the first iteration, $m + y > 0$. So, $m$ increases on every iteration after the first and eventually becomes greater than $n$. A ranking function for this loop is $\max(n-m+1,0) + \max(1-m-y,0)$ because for all reachable states, either $n-m+1$ is reducing and $1-m-y$ stays constant or $n-m+1$ stays constant and $1-m-y$ reduces from 1 to 0. However, we need an invariant $\inv \equiv y + 1 = z$
76% \mvcom{missing Fig.?}
77to prove its validity (Fig.~\ref{overview:rankingred2}).
78For the rest of this section, we refer to the program in Fig.~\ref{overview:code3}
79% \mvcom{again this should be program in Fig. ..}
80as $\pgm$, and the loop-body (lines 6-8) as $\pgm_1$.
81
82% \begin{align*}
83% \qquad&\rf(m’, y’, z’, n’) \\
84% &= \max\big(1-(m’+y’), 0\big) + \max(n’ - m’ + 1, 0) \\
85% &= \max\big(1-2m-y-z, 0\big) + \max(n-2m-y+1,0) \\
86% &= \max\big(1-2m-y-\fbox{\textbf{(y+1)}}, 0\big) + \max\big(n-m+1-(m+y),0\big) \\
87% &= \max(-2m-2y, 0) + \max\big(n-m+1-(m+y),0\big) \\
88% &= 0 +\max\big(n-m+1-(m+y),0\big) \\
89% &= \max\big(n-m+1-(m+y),0\big) \\
90% &\leq \rf(m, y, z, n) - 1
91% \end{align*}
92% \sgcom{The fig shows the derivation of the rf value after the iteration, not exactly that it reduces}.
93
94% As explained before, in the case of a single loop, we can omit $t, T$ from the algorithm state to avoid redundancy as it is easy to capture the loop body transition semantics $\bracs \pro$.
95In the case of a single loop, our algorithm is described in Fig.~\ref{fig:overview},
96% \mvcom{missing reference. Also, if the figures are labelled ‘‘Fig.’’, you should refer to them as ‘‘Fig.’’, and if they are labeled as ‘‘Figure’’ then you should refer to them as ‘‘Figure’’.}
97where it suffices to store a set of states $r$ instead of pairs of states $t$. This is because given a state $s$ at the beginning of a loop, the program state $s’$ at the end of one iteration can be computed as $\bracs{\pgm_1} s$. Similarly, instead of storing the annotated program $\annopgm$, we store the invariant $\inv$ of the loop.
98%
99% In the case of a single loop, the annotated loop program $\alooppgm$ contains the loop program and its invariant. So, it suffices to store the invariant of the loop ($\inv$) instead of $\alooppgm$ in the algorithm state.
100The set $r$ is initialized with randomly generated traces by running the program $L$ for fixed iterations. Here, $r = \{(1,2,3,4), (2,2,3,4)\}$; a program state is a tuple ($m, y, z, n$). The invariant is initialized with the set of all states, i.e., $\invar = \true$. For this example, let $\tempr$, the set of candidate ranking functions, be functions of the form $\max(a^1_0 + \sum_j a^1_jx_j, 0) + \max(a^2_0 + \sum_j a^2_jx_j, 0)$ and $\tempi$, the set of possible invariants, be conjunctions of constraints of the form $d_0 + \sum_jd_jx_j \geq 0$, where $a^1_j,a^2_j,d_j \in \mathbb{Z}$ Note that our algorithm can handle more general forms of ranking functions and invariants that satisfy the conditions explained in Section~\ref{sec:theory}. Our algorithm finds the ranking function and the corresponding invariant for this example using separate queries, while also exchanging key information amongst different phases in each iteration. This enables an efficient termination analysis (Section~\ref{sec:efficiency}).
101% This leads us to achieve an improvement over the existing termination analysis tools in terms of an upper bound on the number of iterations of the CEGIS loops (Section~\ref{sec:efficiency}).
102% More detailed discussion on this can be found in Section~\ref{sec:efficiency}.
103%
104The exact steps for our running example are explained below and also displayed in Table~\ref{tab:overview1}.
105% in the following steps (as displayed in Table~\ref{tab:overview1}):
106% \mvcom{Why does Table~\ref{tab:overview1} appear before the program?}
107\myparagraph{Iteration 1} First, we get a candidate ranking function that reduces for all states in $r$.
108Specifically, we find a satisfying assignment for the coefficients $a^i_j$’s
109% \mvcom{$d_i$’s, perhaps?}
110that satisfy the following query.
111% based on Equation~\ref{eq:rfcreate}. \mvcom{This equation is 2 pages back. We may need to add a page reference, if we need to refer to it. Or we can just explain in words.}
112We do not have to check the bounded condition because all of the functions of the template are bounded by 0.
113% We get the coefficients $a_i$s and $b_i$s for our ranking function template by solving the following SMT query based on the semantics defined in Equation~\ref{eq:rfcreate}:
114 \begin{gather*}
115 \forall (m,y,z,n) \in r \cdot \big( f(m,y,z,n) - f(\bracs{\pgm_1} (m,y,z,n))\geq 1 \big)
116 \end{gather*}
117% where our template $f =\max(a_0 + \sum_i a_ix_i, 0) + \max(b_0 + \sum_i b_ix_i, 0)$.
118We solve this query using Z3~\cite{z3} and obtain $f(m,y,z,n) = \max(n-m+1,0)$.
119% Using the Z3 solver, we get the ranking function $f(m,y,z,n) = \max(n-m+1,0)$.
120%
121Now, we check the candidate function’s validity w.r.t the current invariant $\invar = \true$. This can be done by checking the satisfiability of the following formula.
122% (based on the negation of Equation~\ref{eq:rfcheck}). \mvcom{same comment about page reference for this equation. Also both equations are for the case when the under-approximation is a set of pairs not a set of states.}
123\begin{gather*}
124 \forall (m,y,z,n) \cdot \big((m+y\geq 0) \wedge (m\leq n)\big) \implies \big( f(m,y,z,n) - f(\bracs{\pgm_1} (m,y,z,n))\geq 1 \big)
125\end{gather*}
126% \begin{gather*}
127% (m,y,z,n) \in \inv \wedge \beta(m,y,z,n) \wedge \big(f(m,y,z,n) - f(m’,y’,z’,n’) < 1\big), \quad \text{where} \\
128% \beta(m,y,z,n) = (m+y \geq 0 \wedge m \leq n), \; f(m,y,z,n) = \max(n-m+1,0)
129% % \\ m’=2m+y, \ y’=z, \ z’=z+1, \ n’=n
130% \end{gather*}
131% where $m, y, z, n$ are symbolic variables representing the literal state at the beginning of the loop and $m’=2m+y, \ y’=z, \ z’=z+1, \ n’=n$, which are obtained by symbolically executing the loop body.
132Solving this gives a counter-example $p_1 = (1,-1,2,4)$.
133Next, we refine the algorithm state. There are two possibilities as discussed above. Either $p_1$ is a reachable state and the ranking function is invalid, or $p_1$ is not reachable. We first try to strengthen $\inv$ to $\inv’$ s.t. $p_1 \notin \inv’$. This is done in 2 phases:
134
135
136% Next, first we try to find an invariant $\inv’$ that does not include $c_1$ so that our counter-example pair $(c_1, c_1’)$ can be excluded. We iteratively perform the two phases involved in refining the algorithm state. \\
137% Our algorithm does this by performing these two steps iteratively:\\
138\myparagraph{Generate Invariant Phase} We generate a candidate invariant $ \inv’’$ that includes all states $s$ such that $s \in r$ and does not include the state $p_1$. Here, $\rf$ tries to guide the refinement of an invariant that can prove its validity. This is done by solving the following query for the coefficients $d_j$ to get $\inv’’$ and then taking a conjunction with $\inv$, i.e., $\inv’ = \inv’’ \wedge \inv$.
139\begin{gather*}
140 (1, -1, 2, 4) \notin \invar’’ \wedge \big( \forall (m,y,z,n) \in r \cdot (m,y,z,n) \in \invar’’ \big) \\
141 where \quad (m,y,z,n) \in \invar’’ \ \equiv \ d_0 + d_1m + d_2y + d_3z + d_4n \geq 0
142\end{gather*}
143Solving the above query, we get $\inv’’ \equiv y-z+1 \geq 0$. We now proceed to check the validity of $\inv’$.
144\myparagraph{Check Invariant Phase}
145The validity of the invariant $\invar’$ is checked by solving for a counter-example for the following query.
146Here, $\ini$ is the set of states before the loop at line 3 executes.
147% \mvcom{$\init$ not given for this examples as far as I can tell.}
148\begin{gather*}
149 \big(\forall s \in \init, s \in \invar’\big) \wedge \big(\forall s \in \invar’ \implies \bracs{\pgm_1}s \in \invar’\big), \text{ where }\ini = \{(m,y,z,n) | (y=n) \wedge (z=n+1)\}
150\end{gather*}
151%
152% where $v$ represents symbolic variables generated to represent the state before the loop body and $v’$ represents the values obtained after symbolically executing the loop body on these variables.
153% If we do not get a counter-example, we have successfully refined the invariant. Otherwise, we generate a new candidate invariant that removes this new counter-example and check again until we either find a valid invariant or get \texttt{unsat} while generating the invariant, in which case no such invariant is possible.
154In our example, we do not get a counterexample, and hence, $y-z+1 \geq 0$ is a valid invariant.
155%
156As described above, we guide the invariant search to find an invariant that excludes $p_1$. We update the algorithm state by changing $\inv$ to $\inv’$. Since we store $\inv’$ in the algorithm state, future iterations of the invariant generation phase in our algorithm will start with $\inv’$ instead of $\true$ when trying to determine the reachability of another counter-example. This is in contrast to algorithms~\cite{dynamite,terminator} that rely on external solvers to find invariants because the external solvers do not have information about the previous iterations.
157
158\myparagraph{Iteration 2}
159As the set $r$ is unchanged, we do not generate a new ranking function and directly move on to checking the validity of the ranking function w.r.t the new invariant.
160% the Generate Candidate phase generates the same function $r_f = \max(n-m+1,0)$ and checks its validity w.r.t the new invariant $y + 1 \geq z$ to
161We get a new counter-example $p_2 = (1,-1,-1,1)$.
162% \mvcom{pair?}
163\myparagraph{Generate Invariant Phase} We try to strengthen our invariant $y + 1 \geq z$ to exclude $p_2$ by generating a candidate invariants guided by $p_2$. We generate the candidate $m-n-1 \ge 0$, which includes the states in $r$ but excludes $p_2$.
164\myparagraph{Check Invariant Phase} When checking the validity of the new invariant, we find the counter-example $q_2^1 = (1,1,2,1)$.
165% There are two types of counter-examples we can find when checking the validity of a candidate invariant:
166% \begin{enumerate}
167% \item A pair of states, $(s,s’)$ such that $s \in \invar’$, $s \notin \invar’$ and $s’ = \bracs \pgm s$
168% \item A state, $s$, in $\init$ that is not included in $\invar’$.
169% \end{enumerate}
170% In the first case, we go back to the Generate Invariant Phase and add the additional constraint that for all future invariants generated, $I’’$, $I’’(s_2) \implies I’’(s’_2)$. This condition prevents the same candidate invariant from being generated twice.
171% The counter-example we obtained, (1,0,1,1), falls under the second case because it is in $\init$ but not include in $\invar’$.
172Since $q_2^1 \in \init$,
173% \mvcom{can’t seem to find $\init$. Also, is this claim right? It seems that when we start we have y=n and z=n+1. Isn’t the tuple $(m,z,y,n)$?}
174it is a reachable state. So, we can add it to $r$ to improve the under-approximation of the reachable states. $q_2^1$ has a property that the other states in $r$ do not, i.e., $m=n$. This guides the generation of candidate ranking functions to reduce on states where $m=n$. Since the new invariant is invalid, we go back to the Generate Invariant Phase with an additional constraint that all candidate invariants should include $q_2^1$.
175 % Since the loop condition is true for this state, we can add ((1,0,1,1),(2,1,2,1)) to $t$. ((1,0,1,1),(2,1,2,1)) is a reachable pair of states that has some property not found in any of the pairs of states in $t$, so adding it to $t$ can guide the search for ranking functions by providing diverse states to the under-approximation in the algorithm state. We then go back to the Generate Invariant Phase and add the additional constraint that for all future invariants generated, $I’’$, $(1,0,1,1) \in I’’$. This condition prevents the same candidate invariant from being generated twice.
176After further iterations of finding and checking candidate invariants, we get the invariant $y + 1 \geq z \wedge y + 1 \leq z$, which excludes $p_2$.
177\myparagraph{Iteration 3}
178The set $r$ is changed from the invariant search, so we generate a new candidate ranking function. Guided by the state $q^1_2$, we get the ranking function $\max(n-m+1,0)$. We check the validity of the ranking function w.r.t the new invariant $y + 1 \geq z \wedge y + 1 \leq z$ to get a new counter-example $p_3 = (1,-1,0,4)$. When refining the algorithm state, we are now unable to find a valid invariant that excludes $p_3$ and thus we can conclude that $p_3$ cannot be excluded from the set of reachable states using any invariant from our template. So, we add it to $r$, refining the algorithm state.
179\myparagraph{Iteration 4} As the set $r$ is updated, we generate a new candidate ranking function $\rf = \max(n-m+1,0) + \max(1-m-y, 0)$ that reduces on all states in the updated $r$. We then check its validity w.r.t the current invariant $y + 1 \geq z \wedge y + 1 \leq z$. The validity check succeeds, and $\rf = \max(n-m+1,0) + \max(1-m-y, 0)$ is returned as a valid ranking function for the program.
180
181The above steps demonstrate the benefits of the synergistic approach in finding a ranking function for the loop in Fig.~\ref{overview:code3} and an invariant ($y + 1 = z$) that is useful for proving the validity of the ranking function. Note that there are many valid invariants for this loop, such as $y \leq z$, $y \geq n$, $z \geq n + 1$, etc. However, they do not help in finding or proving the validity of the ranking function. The counter-examples found when checking the validity of candidate ranking functions guide the search for stronger invariants, as shown in iterations 1 and 2 above. Further, the counter-examples found when checking the validity of candidate invariants guide the search for a valid ranking function, as shown in iterations 2 and 3 above.
182
183\subsection{Nested Loops}
184\label{sec:nestedloops}
185\begin{wrapfigure}{l}{0.4\linewidth}
186\begin{lstlisting}[numbers=left,basicstyle=\ttfamily\footnotesize,backgroundcolor=\color{backcolour}]
187 y = n;
188 z = n+1;
189 while (y+n+1 >= k*k+z && y == z+1){
190 while (m+y >= 0 && m <= n){
191 m = 2*m + y;
192 y = z;
193 z = z+1;
194 }
195 y++;
196 z++;
197 n--;
198 }\end{lstlisting}
199\caption{Nested loop program}
200\label{fig:nest}
201\end{wrapfigure}
202\noindent
203When considering nested loops, instead of storing $r$, an under-approximation of the reachable states, we have to store $t$, which contains pairs of states, and serves as an under-approximation of the transition relation of the loop because we can no longer directly compute the program state at the end of the loop given the program state at the beginning.
204For instance, consider the program $\pgm$ in Fig.~\ref{fig:nest}.
205% \mvcom{reference number seems to be off.}
206$\pgm_i$ is the inner loop (lines 4-8),
207% \mvcom{is the loop body of the inner loop? If so should it be lines 5 to 7?},
208$\beta_o$ and $\beta_i$ are the loop guards at lines 3 and 4 respectively. Given a program state $s$ before executing the inner loop at lines 4-8, we cannot compute the state $s’$ just before line 9. This is because $\bracs{\pgm_i}$ is also unknown. So, we use an invariant $\invar_i$ to over-approximate $\bracs{\pgm_i}$. Similarly, we use an invariant $\invar_o$ for the outer loop. Note that the initial set for $\invar_i$ depends on $\invar_o$. Conversely, $\invar_o$ depends on $\bracs{\pgm_i}$ which is approximated using $\invar_i$. So, the invariants corresponding to all the loops in a program depend on each other.
209%
210Since we approximate the transition relation $\bracs{P}$ using a subset of pairs of reachable states $t$, and the invariants ($\invar_i, \invar_o$), we represent our algorithm state as $\langle t, (\invar_o, \invar_i) \rangle$.
211%
212While this algorithm state works for this example, it needs to be generalized to programs with arbitrary nested or sequential loops. We achieve this generalization using the notion of an annotated program, which is discussed formally in Section~\ref{sec:annotatedpgm}.% For this example (program in Fig.~\ref{fig:nest}), however, we use $\langle t, (\invar_o, \invar_i) \rangle$ as the algorithm state.
213
214% In this setting, for the annotated program, $\alooppgm = \invar \; @ \; \texttt{while}(\beta) \texttt{ do }\anno \texttt{ od}$, where $\anno$ also contains loops. Consider the loop $L$ at line 3 in Fig.~\ref{fig:nest}. We create a corresponding annotated program $\alooppgm$ where the invariants at lines 3 and 4 are initialized as sets of all states, i.e., $\invar_o = \invar_i = \true$.
215% Since we approximate the transition relation $\bracs{P}$ using a subset of pairs of reachable states ($t$), and the invariants ($\invar_i, \invar_o$), we represent our algorithm state as $\langle t, (\invar_o, \invar_i) \rangle$. \mvcom{Earlier in the paper we use annotated program as the second component. Here we are using a pair of invariants. Perhaps a holdover from old version of the paper.}
216Note that here we will use the same templates $\tempr$ and $\tempi$ for both loops, but this is not a requirement for our algorithm.
217Both invariants are initialized as the set of all states, i.e., $\invar_o = \invar_i = \true$.
218Using this, we compute an initial set $\init_i$ for the inner program $\pgm_i$. In this case, $\init_i = \invar_o \cap \bracs{\beta_o} = \{(m,y,z,n) | (y+n+1 \ge k*k+z) \wedge (y=z+1)\}$. The initial set $\init_o$ for the outer while loop is $\{(m,y,z,n) | (y=n) \wedge (z=n+1)\}$.
219% \mvcom{Should we use $\init_o$ to be consistent with the rest of the notation?}
220We can start by searching for a ranking function for either the outer or inner loop first. We choose the inner loop. Since the body of the inner loop is the same as the loop body in the program in Fig.~\ref{overview:code3} and $\init_i$ is a subset of the $\init$ set we computed when analyzing the single loop case, we can go through the same iterations as above to get $\rf_i = \max(n-m+1,0) + \max(1-m-y, 0) $, $\invar_i \equiv y + 1 = z$, and $\invar_o = \true$.
221% As the inner loop of the program is the same as the program in Fig.~\ref{overview:code3}, we get $\rf_i = \max(n-m+1,0) + \max(1-m-y, 0) $, $\invar_i = (y + 1 \geq z) \wedge (y + 1 \leq z) \equiv y + 1 = z$, and $\invar_o = \true$.
222Next, \toolname uses similar steps as discussed in Section~\ref{sec:example} to find a ranking function for the outer loop: \\
223(1) We generate a candidate ranking function $\rf$ similar to the single loop case. The one thing that changes while validating $\rf$ is that because we have a loop in the body of the outer loop, we can not symbolically execute to find the program state at the end of one iteration.
224% For e.g., consider that we have a candidate ranking function $\rf$ for the outer loop along with the two invariants $\invar_o$ and $\invar_i$ and we need to check its validity. We can no longer define symbolic variables $m,y,z,n,k$ and do a symbolic execution of the loop body to get $m’, y’, z’, n’, k’$ as we have the inner loop.
225To get through this, we define fresh variables $m’’, y’’, z’’, n’’, k’’$ to represent the state just after the inner loop ends and assume that this state satisfies $\invar_i \wedge \neg \beta_i$, and
226% \avcom{symbolic state?}
227% (where $\beta_i$ is the loop guard of the inner loop).
228% Using this, we
229define the validation query as:
230% We then analyze $\anno$ find valid invariants $\invar_i$ and $\invar_o$ and a ranking function $\rf_i$ that is valid w.r.t $\init$, $\invar_i$ and $\invar_o$. We use $\invar_o$ to over-approximate the set of initial states for the inner loop.
231% \textcolor{red}{Aval: previous line is unclear.}
232% Next, we try to find a ranking function for the outer loop.
233% For the outer loop, it is hard to compute the exact transition relation of the loop body because the loop body itself has a loop. This makes it more challenging to generate and check the validity of candidate ranking functions.
234% % To tackle this, our algorithm generates candidate ranking functions for nested loops using samples from the execution traces ($t$), that serve as an under-approximation of $\bracs \prog$ (where $\prog$ is the program at lines 4 to 11).
235% To check the validity of ranking functions, we use $\invar_i$ to over-approximate $\bracs{\prog}$. Since we need both invariants for both loops, while finding the ranking function for each loop, we can choose to refine either $\invar_i$ or $\invar_o$ when we refine the algorithm state.
236% \textcolor{red}{Aval: Need to change the previous few lines. It is repetition.}
237% To check the validity of ranking functions, we use the invariant generated for the inner loop in $\anno$ to over-approximate the transition relation induced by $\anno$ using the notion of $\bracs \anno$ (defined in Section~\ref{sec:background}).
238
239
240\begin{table}
241 \centering
242 \resizebox{\textwidth}{!}{
243 \begin{tabular}{@{}lrrrr@{}}
244 \hline
245 &$t$ & $(\invar_o,\invar_i)$ & $\rf$ & $p, p’$ \\
246 \hline
247 \multirow{2}{*}{1}&$\{((2,2,3,4,1),(6,7,8,0,1)),$ & \multirow{2}{*}{$(\true, y + 1 = z)$} & \multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,4,5,5), (7,2,3,5,5)$} \\
248 &$((2,2,3,5,1), (6,8,9,0,1))\}$ & & & \\
249 \hline
250 \multirow{2}{*}{2}&$\{((2,2,3,4,1),(6,7,8,0,1)),$ & \multirow{2}{*}{($\textcolor{blue}{y+1\geq z}, y+1=z)$} & \multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,2,5,5), (8,3,4,5,5)$} \\
251 &$((2,2,3,5,1), (6,8,9,0,1))\}$ & & & \\
252 \hline
253 \multirow{2}{*}{3}&$\{((2,2,3,4,1),(6,7,8,0,1)),$ & \multirow{2}{*}{(
254 $\textcolor{blue}{(y+1\geq z) \wedge (y+1\leq z)}$, y + 1 = z)} & \multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,3,5,5), (7,5,6,5,5)$} \\
255 &$((2,2,3,5,1), (6,8,9,0,1))\}$ & & & \\
256 \hline
257 \multirow{3}{*}{4}&$\{((2,2,3,4,1),(6,7,8,0,1)), $ & \multirow{3}{*}{$((y\geq z-1) \wedge (y\leq z-1), y+1=z)$} & \multirow{3}{*}{$\textcolor{blue}{\max(n-k+1,0)}$} & \multirow{3}{*}{-} \\
258 &$((2,2,3,5,1), (6,8,9,0,1)),$ & & & \\
259 &$\textcolor{blue}{((1,2,3,5,5),(7,5,6,5,5))}\}$ & & & \\
260 \hline
261 \end{tabular}
262 }
263 \caption{Steps taken by \toolname to prove the termination for the program in Fig.~\ref{fig:nest}}
264 \label{tab:overview2}
265\end{table}
266
267% \begin{table}
268% \centering
269% \resizebox{\textwidth}{!}{
270% \begin{tabular}{@{}lrrrr@{}}
271% \hline
272% &$t$ & $(\invar_o,\invar_i)$ & $\rf$ & $p, p’$ \\
273% \hline
274% 1&$\{((2,2,3,4,1),(6,7,8,0,1)),((2,2,3,5,1), (6,8,9,0,1))\}$ & $(\true, y + 1 = z)$ & $\max(n-k,0)$ & $(1,2,4,5,5), (7,2,3,5,5)$ \\
275% % &$((2,2,3,5,1), (6,8,9,0,1))\}$ & & & \\
276% \hline
277% 2&$\{((2,2,3,4,1),(6,7,8,0,1)),((2,2,3,5,1), (6,8,9,0,1))\}$ & $(\textcolor{blue}{y + 1 \geq z}, y + 1 = z)$ & $\max(n-k,0)$ & $(1,2,4,5,5), (7,2,3,5,5)$ \\
278% \hline
279% % \multirow{2}{*}{2}&$\{((2,2,3,4,1),(6,7,8,0,1)),$ & \multirow{2}{*}{($\textcolor{blue}{y+1\geq z}, y+1=z)$} & \multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,2,5,5), (8,3,4,5,5)$} \\
280% % &$((2,2,3,5,1), (6,8,9,0,1))\}$ & & & \\
281% % \hline
282% 3&$\{((2,2,3,4,1),(6,7,8,0,1)),((2,2,3,5,1), (6,8,9,0,1))\}$ & $(\textcolor{blue}{(y + 1 \geq z)\wedge (y + 1 \leq z)}, y + 1 = z)$ & $\max(n-k,0)$ & $(1,2,4,5,5), (7,2,3,5,5)$ \\
283% \hline
284% % \multirow{2}{*}{3}&$\{((2,2,3,4,1),(6,7,8,0,1)),$ & \multirow{2}{*}{(
285% % $\textcolor{blue}{(y+1\geq z) \wedge ((y+1\leq z)}$, y + 1 = z)} & \multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,3,5,5), (7,5,6,5,5)$} \\
286% % &$((2,2,3,5,1), (6,8,9,0,1))\}$ & & & \\
287% % \hline
288% \multirow{2}{*}{4}&$\{(2,2,3,4,1),(6,7,8,0,1)), ((2,2,3,5,1), (6,8,9,0,1)), $ & \multirow{2}{*}{$((y\geq z-1) \wedge (y\leq z-1), y+1=z)$} & \multirow{2}{*}{$\textcolor{blue}{\max(n-k+1,0)}$} & \multirow{2}{*}{-} \\
289% &$\textcolor{blue}{((1,2,3,5,5),(7,5,6,5,5)}\}$ & & & \\
290% \hline
291% \end{tabular}
292% }
293% \caption{Steps taken by \toolname to prove the termination for the program in Fig.~\ref{fig:nest}}
294% \label{tab:overview2}
295% \end{table}
296
297
298
299
300% At each step, the algorithm state is defined by $\langle t, \anno_l \rangle$.
301% The annotations of $A_l$ have the invariants for the two loops.
302% Since we approximate the transition relation $\bracs{P}$ using a subset of pairs of reachable states ($t$), and the invariants ($\invar_i, \invar_o$), we represent our algorithm state as $\langle t, (\invar_o, \invar_i) \rangle$. $\invar_{o}$ and $\invar_i$ are initialized with the output obtained by solving the inner loop ($\invar_i$).
303% Note that here we will use the same templates $\tempr$ and $\tempi$ for both loops, but this is not a requirement for our algorithm.
304
305
306\begin{gather*}
307 \invar_o(m,y,z,n,k) \wedge \beta_o(m,y,z,n,k) \wedge \big(f(m,y,z,n,k) - f(m’,y’,z’,n’,k’) < 1\big) \; \wedge \\
308 \invar_i(m’’,y’’,z’’,n’’,k’’) \; \wedge \; \neg \beta_i(m’’,y’’,z’’,n’’,k’’), \quad \text{where} \\
309 % \beta_o(m,y,z,n,k) = (y+n+1 \geq k^2 + z), \quad \beta_i(m’’,y’’,z’’,n’’,k’’) = (m’’+y’’ \geq 0 \wedge m’’ \leq n’’), \\
310 m’ = m’’, \ y’ = y’’ + 1, \ z’ = z’’ + 1, \ n’ = n’’ - 1, \ k’ = k’’
311 % \\ m’=2m+y, \ y’=z, \ z’=z+1, \ n’=n
312\end{gather*}
313\noindent
314(2) We refine the state of the algorithm. From the above validation query, we get a counter-example of the form $(p, p’’, p’)$. Here $p$ and $p’$ are the states at the beginning and end of one iteration of the outer loop, and $p’’$ is the state at the exit of the inner loop. So, the refine phase has two options: (a) either refine the outer invariant $\invar_o$ first to exclude $p$ or (b) refine the inner invariant $\invar_i$ to exclude $p’’$. If at least one of the invariants is refined, we check the validity of the ranking function again. If it is not possible to refine either of the invariants, we add $(p, p’)$ to t. Once we choose an invariant to refine, we iteratively go through the Generate Invariant Phase and the Check Invariant Phase. If the invariant we chose cannot be refined, we try to refine the other invariant.
315%
316Table~\ref{tab:overview2} gives the steps our algorithm takes to find the ranking function for the outer loop.
317This approach can be generalized to nested loops with arbitrary depth as explained in Section ~\ref{sec:theory}.
318% The approach described above can be generalized to any number of nestings. Consider again a loop program of the form $\anno_l = \invar \; @ \; \texttt{while}(\beta) \texttt{ do }\anno \texttt{ od}$. Our algorithm will first prove the termination of all the loops present in $\anno$ and simultaneously finds invariants for all of them. Once this is done, we can then analyze $\anno_l$ using the invariants of the inner loops to over-approximate the transition relation of $\anno$ using $\bracs \anno$. In the refine phase in this case, either we refine the invariant of $\anno_l$ or at least one of the inner loop invariants is refined to exclude the counter-example sequence.
319
320% Say the program has $n$ nested loops $L_1, L_2, \cdots L_n$. Our algorithm starts with the innermost loop $L_n$ and finds a ranking function and an invariant ($I_n$) that validates it. We then shift to loop $L_{n-1}$. In general, to prove the termination of loop $L_i$, we maintain a tuple of invariants $(I_i, I_{i+1}, \cdots I_n)$ (one for each loop inside
321% and including $L_i$) that over-approximates the program transitions ($\trans$) and the set of reachable states of $L_i$. Then we iteratively try to find a ranking function ($\rf$) from the traces of this loop and keep refining the tuple of invariants $(I_i, I_{i+1}, \cdots I_n )$ until we find a ranking function $\rf$ and the set of invariants that can prove the termination of this loop. This is inductively done for all the loops till $L_1$.
322
323\subsection{Theoretical Guarantees}
324Based on the assumption that the template of ranking functions incorporates a finite set of possibilities and that the template for invariants is closed under intersection and does not have an infinite descending chain (w.r.t the partial order defined in Section~\ref{sec:theory}), we establish the soundness and relative completeness of \toolname (as detailed in Section~\ref{sec:efficiency}). Specifically, if there exist a valid ranking function and an invariant from their respective templates for each loop that can prove their termination, then \toolname will be able to prove their termination. Conversely, in cases where no valid ranking function exists for a loop w.r.t any invariants across all loops, \toolname terminates without asserting the termination.
325% of the given program.
326% We used specific templates for ranking functions and invariants above, but these templates can be generalized as long as the ranking function template is finite, the invariant template is closed under intersection and the partial order on the elements of the invariant template does not contain an infinite descending chain. In Section~\ref{sec:theory}, we prove that under certain assumptions, if there exist valid ranking functions and invariants from their respective templates for each loop that can prove their termination, then our algorithm will be able to prove their termination. We also prove that if there is no ranking function for a loop that is valid w.r.t. any sequence of invariants for all of the loops, our algorithm will still terminate.
327
328% In the example above, we used specific templates for ranking functions and invariants. These templates can be generalized to many other templates, as long as they satisfy the following conditions:
329% \begin{enumerate}
330% \item The template of invariants ($\tempi$) is closed under intersection
331% \item The elements in $\tempi$ are partially ordered by the $\subseteq$ ordering and there is no infinite descending chain in $\tempi$.
332% \item The template for ranking functions ($\tempr$) is finite.
333% \item Given a valid invariant, $\invar$, and a program state $c$, it is possible to sample a valid invariant, $\invar’$ such that $\invar’ \subseteq \invar \setminus \{c\}$ iff such an invariant exists or determine that no such invariant exists within finite time.
334% \item Given a relation, $t$, we can find a ranking function $f \in \tempr$ that reduces and is bounded on $t$.
335% \item The validity-check of a ranking function w.r.t. a set of states and a transition relation falls in a decidable theory.
336% \end{enumerate}
337% If the above conditions hold, we prove that the algorithm is sound and complete in Section~\ref{sec:theory}.

3. Preliminaries

Relations

For a pair of binary relations R1⊆A×BR_{1}\subseteq A\times B and R2⊆B×CR_{2}\subseteq B\times C, their composition is the relation R1∘R2={(a,c)|∃b∈B.(a,b)∈R1​ and ​(b,c)∈R2}⊆A×CR_{1}\circ R_{2}=\{(a,c)\>|\>\exists b\in B.\ (a,b)\in R_{1}\text{ and }(b,c)\in R_{2}\}\subseteq A\times C. For a set S⊆AS\subseteq A and a binary relation R⊆A×BR\subseteq A\times B, S∘R={b∈B|∃a∈S.(a,b)∈R}S\circ R=\{b\in B\>|\>\exists a\in S.\ (a,b)\in R\} denotes the image of SS under RR. Finally, for a set AA, the identity relation on AA is denoted as 𝗂𝖽A={(a,a)|a∈A}\mathsf{id}_{A}=\{(a,a)\>|\>a\in A\}.

While Programs

To illustrate our synergistic synthesis approach, we will consider programs in a simple while programming language whose BNF grammar is given below. In what follows, xx is a program variable, ee a program expression and β\beta a Boolean expression. The syntax of expressions is not given as it is not important to the main ideas of this paper.

𝖯::=skip|x←e​|𝖯​;​𝖯|​if ​β​ then ​𝖯​ else ​𝖯|while ​β​ do ​𝖯​ od\begin{array}[]{rcl}\mathsf{P}&::=&\texttt{skip}\ |\ x\leftarrow e\ |\ \mathsf{P}\>\text{;}\>\mathsf{P}\ |\ \texttt{if }\beta\texttt{ then }\mathsf{P}\texttt{ else }\mathsf{P}\ |\ \texttt{while }\beta\texttt{ do }\mathsf{P}\texttt{ od}\end{array}

A loop-free program code is one that does not have any while-loops. We will typically use 𝖯,𝖯1,𝖯2,…\mathsf{P},\mathsf{P}_{1},\mathsf{P}_{2},\ldots to denote programs, α,α1,…\alpha,\alpha_{1},\ldots to denote loop-free programs, and 𝖫,𝖫1,…\mathsf{L},\mathsf{L}_{1},\ldots to denote loops, i.e., programs of the form while ​β​ do ​𝖯​ od\texttt{while }\beta\texttt{ do }\mathsf{P}\text{ od}.

Towards defining the semantics for a program 𝖯\mathsf{P}, it is useful to introduce the notion of a program state. A program state ss of 𝖯\mathsf{P} assigns values to each variable of 𝖯\mathsf{P}. The set of program states of 𝖯\mathsf{P} will be denoted as S𝖯S_{\mathsf{P}}. When the program 𝖯\mathsf{P} is clear from the context, we will abuse notation and simply use SS to denote all possible program states of 𝖯\mathsf{P}, which is represented by the invariant 𝖨𝗍𝗋𝗎𝖾\mathsf{I}_{\mathsf{true}}. The semantics of a program 𝖯\mathsf{P} denoted ⟦𝖯⟧\llbracket\mathsf{P}\rrbracket, is a binary relation on SS that captures how a program state is transformed when 𝖯\mathsf{P} is executed. Assuming standard expressions and their semantics, one can naturally define the semantics of loop-free programs. Loops present a challenge. We will use invariants to over-approximate their semantics. This is also the reason why we will use relational semantics, as opposed to partial functions.

4. Annotated Programs

As explained in Sections LABEL:sec:nestedloops and  3, in our approach, we approximate the reachable states and the semantics of loops using invariants. So, it is useful to associate invariants with each loop in the program. The set of invariants used to annotate loops will be from a template language. Let us fix a collection ℐ⊆2S\mathcal{I}\subseteq 2^{S} of invariants, where SS is the set of program states. For technical reasons that we will emphasize later, we will assume that ℐ\mathcal{I} is closed under intersection. That is, for any 𝖨1,𝖨2∈ℐ\mathsf{I}_{1},\mathsf{I}_{2}\in\mathcal{I}, 𝖨1∩𝖨2∈ℐ\mathsf{I}_{1}\cap\mathsf{I}_{2}\in\mathcal{I}. Using the invariants in ℐ\mathcal{I}, we define annotated programs as programs defined by the BNF grammar below, where 𝖨\mathsf{I} is a member of ℐ\mathcal{I}.

𝖠::=skip|x←e​|𝖠​;​𝖠|​if ​β​ then ​𝖠​ else ​𝖠|𝖨​@​while ​β​ do ​𝖠​ od\begin{array}[]{rcl}\mathsf{A}&::=&\texttt{skip}\ |\ x\leftarrow e\ |\ \mathsf{A}\>\text{;}\>\mathsf{A}\ |\ \texttt{if }\beta\texttt{ then }\mathsf{A}\texttt{ else }\mathsf{A}\ |\ \mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}\texttt{ od}\end{array}

The main difference between (unannotated) programs and the above grammar is that loops are annotated with an invariant as in the case 𝖨​@​while ​β​ do ​𝖠​ od\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}\texttt{ od}. We will use 𝖠,𝖠1,…\mathsf{A},\mathsf{A}_{1},\ldots to denote annotated programs. For an annotated program 𝖠\mathsf{A}, its underlying program can obtained by removing the invariant annotations on the while-loops and we denote this as 𝒞​(𝖠)\mathcal{C}(\mathsf{A}). This is defined in the Appendix A (Definition A.1). For a (unannotated) program 𝖯\mathsf{P}, the collection of all annotated programs over 𝖯\mathsf{P} will be denoted by 𝖠​(𝖯)\mathsf{A}(\mathsf{P}), i.e., 𝖠​(𝖯)={𝖠|𝒞​(𝖠)=𝖯}\mathsf{A}(\mathsf{P})=\{\mathsf{A}\>|\>\mathcal{C}(\mathsf{A})=\mathsf{P}\}. We will use 𝖠𝖫\mathsf{A}_{\mathsf{L}} to denote an annotated subprogram of 𝖠\mathsf{A} that corresponds to the loop 𝖫\mathsf{L} in 𝖠\mathsf{A}.

In the following Sections, we show how to use the invariants associated with each loop. Primarily, they have two use cases - (i) over-approximating the transition relation of a loop (Section 4.1), (ii) over-approximating the set of initial states for each loop (Section 4.2). Then we describe how to use annotated programs to define the validity of ranking functions (Section 4.3). We also define a partial order and meet operation over them (Section 4.4). Using these definitions, we ensure that Syndicate refines the state in each iteration and is complete even for arbitrarily nested loops.

4.1. Semantics of Annotated Programs

To define the approximate semantics of an annotated program 𝖠\mathsf{A} that captures the terminating computations of 𝖠\mathsf{A}, we assume a standard semantics of program expressions and Boolean expressions which can be used to define the semantics of loop-free programs in a natural way. We take ⟦α⟧\llbracket\alpha\rrbracket to be the transition semantics of a loop-free program α\alpha and ⟦β⟧⊆S\llbracket\beta\rrbracket\subseteq S to be the semantics of a Boolean expression β\beta. The semantics of an annotated program 𝖠\mathsf{A} is defined inductively as follows.

⟦α⟧\displaystyle\llbracket\alpha\rrbracket ≜⟦α⟧\displaystyle\triangleq\ \llbracket\alpha\rrbracket
⟦if ​β​ then ​𝖠1​ else ​𝖠2⟧\displaystyle\llbracket\texttt{if }\beta\texttt{ then }\mathsf{A}_{1}\texttt{ else }\mathsf{A}_{2}\rrbracket ≜𝗂𝖽⟦β⟧∘⟦𝖠1⟧∪𝗂𝖽⟦¬β⟧∘⟦𝖠2⟧\displaystyle\triangleq\ \mathsf{id}_{\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}_{1}\rrbracket\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ\llbracket\mathsf{A}_{2}\rrbracket
⟦𝖠1;𝖠2⟧\displaystyle\llbracket\mathsf{A}_{1}\>;\>\mathsf{A}_{2}\rrbracket ≜⟦𝖠1⟧∘⟦𝖠2⟧\displaystyle\triangleq\ \llbracket\mathsf{A}_{1}\rrbracket\circ\llbracket\mathsf{A}_{2}\rrbracket
⟦𝖨​@​while ​β​ do ​𝖠1​ od⟧\displaystyle\llbracket\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}_{1}\texttt{ od}\rrbracket ≜𝖨×(𝖨∩⟦¬β⟧)\displaystyle\triangleq\ \mathsf{I}\times(\mathsf{I}\cap\llbracket\neg\beta\rrbracket)

The difference between the semantics of an annotated program and that of a regular (unannotated) program lies in the case of loops: ⟦𝖨​@​while ​β​ do ​𝖠1​ od⟧\llbracket\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}_{1}\texttt{ od}\rrbracket. We can over-approximate the semantics of the loop body ⟦𝖠1⟧\llbracket\mathsf{A}_{1}\rrbracket using the associated invariant 𝖨\mathsf{I}. The reachable states, ℛ\mathcal{R}, at the entry of the while-loop, must satisfy the invariant. So, ℛ⊆𝖨\mathcal{R}\subseteq\mathsf{I}. The states that satisfy β\beta enter the loop, while the states that do not satisfy β\beta exit. So, the transition relation is over-approximated by 𝖨×(𝖨∩⟦¬β⟧)\mathsf{I}\times(\mathsf{I}\cap\llbracket\neg\beta\rrbracket).

4.2. Correctness of Annotated Programs

Annotations of invariants in an annotated program 𝖠\mathsf{A} are expected to be inductive loop invariants for the while-loops they decorate. Without such an assumption, the semantics defined in the previous paragraph will not accurately describe the terminating computations of the program. Recall that an inductive invariant 𝖨\mathsf{I} is a set of program states that satisfies the following two properties: (Initiation) 𝖨\mathsf{I} contains all program states you could enter the loop in; (Consecution) If you run the loop body from a state in 𝖨\mathsf{I}, you end up in a state that also belongs to 𝖨\mathsf{I}. Based on this, we can define what it means for all the annotations in a program to be correct. Notice that correctness needs to be defined w.r.t a set of initial states. Let I​n​i​t⊆SInit\subseteq S be a set of initial program states and let 𝖠\mathsf{A} be an annotated program. 𝖠\mathsf{A} is said to be correct with respect to initial states I​n​i​tInit if the annotations in 𝖠\mathsf{A} are inductive invariants. This can be inductively defined based on the structure of 𝖠\mathsf{A}.

I​n​i​t⊧α\displaystyle Init\models\alpha ≜𝗍𝗋𝗎𝖾\displaystyle\triangleq\ \mathsf{true}
I​n​i​t⊧if ​β​ then ​𝖠1​ else ​𝖠2\displaystyle Init\models\texttt{if }\beta\texttt{ then }\mathsf{A}_{1}\texttt{ else }\mathsf{A}_{2} ≜(Init∩⟦β⟧⊧𝖠1)∧(Init∩⟦¬β⟧⊧𝖠2)\displaystyle\triangleq\ (Init\cap\llbracket\beta\rrbracket\models\mathsf{A}_{1})\wedge(Init\cap\llbracket\neg\beta\rrbracket\models\mathsf{A}_{2})
I​n​i​t⊧𝖠1;𝖠2\displaystyle Init\models\mathsf{A}_{1}\>;\>\mathsf{A}_{2} ≜(Init⊧𝖠1)∧(Init∘⟦𝖠1⟧⊧𝖠2)\displaystyle\triangleq\ (Init\models\mathsf{A}_{1})\wedge(Init\circ\llbracket\mathsf{A}_{1}\rrbracket\models\mathsf{A}_{2})
I​n​i​t⊧𝖨​@​while ​β​ do ​𝖠1​ od\displaystyle Init\models\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}_{1}\texttt{ od} ≜(Init⊆𝖨)∧((𝖨∩⟦β⟧)∘⟦𝖠1⟧⊆𝖨×𝖨)∧(Init∩⟦β⟧⊧𝖠1)\displaystyle\triangleq\ (Init\subseteq\mathsf{I})\wedge((\mathsf{I}\cap\llbracket\beta\rrbracket)\circ\llbracket\mathsf{A}_{1}\rrbracket\subseteq\mathsf{I}\times\mathsf{I})\wedge(Init\cap\llbracket\beta\rrbracket\models\mathsf{A}_{1})

Note that in the above definition, given an initial set for the annotated program 𝖠𝖫\mathsf{A}_{\mathsf{L}}, we use its constituent invariants to compute the initial set for the annotated subprograms of 𝖠𝖫\mathsf{A}_{\mathsf{L}}. The individual initial sets are consequently used for defining the correctness of the annotated programs. In the case of a loop, where 𝖠𝖫≡𝖨​@​while ​β​ do ​𝖠1​ od\mathsf{A}_{\mathsf{L}}\equiv\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}_{1}\texttt{ od}, the correctness condition also checks the correctness of the invariant 𝖨\mathsf{I}.

4.3. Correctness of Ranking Functions using Annotated Programs

A ranking function is a real-valued function ff on the program states that is bounded from below and decreases by a minimum amount in every iteration of the loop. For such a ranking function ff to be a valid witness for termination, ff is only required to have these properties on the reachable states (or an over-approximation of the reachable states) of the program rather than all the program states. Given these observations, we define when a ranking function proves the termination of an annotated while-loop, given an initial set of states.

Definition 4.0 (Correctness of a Ranking Function).

Let I​n​i​t⊆SInit\subseteq S be a set of initial program states and f:S→ℝf:S\to\mathbb{R} be a candidate ranking function. We say that ff establishes the termination of annotated program 𝖠𝖫=𝖨​@​while ​β​ do ​𝖠​ od\mathsf{A}_{\mathsf{L}}=\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}\texttt{ od} from initial states I​n​i​tInit, i.e., I​n​i​t⊧𝖠𝖫,fInit\models\mathsf{A}_{\mathsf{L}},f if

  • •

    The annotations of 𝖠𝖫\mathsf{A}_{\mathsf{L}} are correct with respect to I​n​i​tInit, i.e., I​n​i​t⊧𝖠𝖫Init\models\mathsf{A}_{\mathsf{L}}, and

  • •

    For all (s,s′)∈𝗂𝖽𝖨∩⁣⟦β⟧∘⟦𝖠⟧(s,s^{\prime})\in\mathsf{id}_{\mathsf{I}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}\rrbracket, f​(s)≥0f(s)\geq 0 and f​(s)−f​(s′)≥1f(s)-f(s^{\prime})\geq 1

Note that in Definition 4.1, we require that the ranking function ff be positive and decrease by 11 in each loop iteration. These may appear to be strong requirements as typically, ranking functions are only required to be bounded above some value (say θ\theta) and decrease by some minimum amount (say δ\delta). However, if such a more general type of ranking function gg exists then the specific one of the type given in Definition 4.1 also exists: just take f​(s)f(s) to be (g​(s)−θ)/δ(g(s)-\theta)/\delta.

4.4. Meet-semilattice on Annotated programs

We introduce a partial order (⪯\preceq) and a meet operation (∧\wedge) for the set of annotated programs (𝖠\mathsf{A}), which are crucial to understanding our algorithm. Let 𝖠\mathsf{A} be an annotated program such that 𝒞​(𝖠)=𝖯\mathcal{C}(\mathsf{A})=\mathsf{P}. For annotated programs 𝖠1,𝖠2∈𝖠​(𝖯)\mathsf{A}_{1},\mathsf{A}_{2}\in\mathsf{A}(\mathsf{P}) (i.e., 𝒞​(𝖠1)=𝒞​(𝖠2)=𝖯\mathcal{C}(\mathsf{A}_{1})=\mathcal{C}(\mathsf{A}_{2})=\mathsf{P}), we say 𝖠2⪯𝖠1\mathsf{A}_{2}\preceq\mathsf{A}_{1} if for each loop in 𝖯\mathsf{P}, the invariant annotating this loop in 𝖠2\mathsf{A}_{2} is contained in the corresponding invariant in 𝖠1\mathsf{A}_{1}; the formal definition is deferred to Appendix A. If 𝖠2⪯𝖠1\mathsf{A}_{2}\preceq\mathsf{A}_{1} and 𝖠2≠𝖠1\mathsf{A}_{2}\neq\mathsf{A}_{1} then we say 𝖠2≺𝖠1\mathsf{A}_{2}\prec\mathsf{A}_{1}. Next, 𝖠1∧𝖠2\mathsf{A}_{1}\wedge\mathsf{A}_{2} denotes the annotated program where each loop is annotated by the intersection of the invariants annotating the loop in 𝖠1\mathsf{A}_{1} and 𝖠2\mathsf{A}_{2}.

In Appendix B, we show that if there are two annotated programs 𝖠1,𝖠2∈𝖠​(𝖯)\mathsf{A}_{1},\mathsf{A}_{2}\in\mathsf{A}(\mathsf{P}) such that they are valid w.r.t the initial set, i.e., I​n​i​t⊧𝖠1Init\models\mathsf{A}_{1} and I​n​i​t⊧𝖠2Init\models\mathsf{A}_{2}, then the meet of 𝖠1\mathsf{A}_{1} and 𝖠2\mathsf{A}_{2} is also valid w.r.t the initial set, i.e., I​n​i​t⊧𝖠1∧𝖠2Init\models\mathsf{A}_{1}\wedge\mathsf{A}_{2}. Further, if 𝖯\mathsf{P} is a loop program, if 𝖠1\mathsf{A}_{1} and a ranking function ff are valid w.r.t to the initial set, i.e. I​n​i​t⊧𝖠1,fInit\models\mathsf{A}_{1},f, and 𝖠2\mathsf{A}_{2} is a valid annotated program w.r.t I​n​i​tInit and 𝖠2⪯𝖠1\mathsf{A}_{2}\preceq\mathsf{A}_{1}, then the pair 𝖠2,f\mathsf{A}_{2},f is also valid w.r.t I​n​i​tInit. This can formally be presented as:

Proposition 4.0.

Let 𝖠1,𝖠2∈𝖠​(𝖯)\mathsf{A}_{1},\mathsf{A}_{2}\in\mathsf{A}(\mathsf{P}) be two annotated programs.

  1. (1)

    If I​n​i​t⊧𝖠2Init\models\mathsf{A}_{2} and I​n​i​t⊧𝖠1Init\models\mathsf{A}_{1}, then I​n​i​t⊧𝖠1∧𝖠2Init\models\mathsf{A}_{1}\wedge\mathsf{A}_{2}.

  2. (2)

    If I​n​i​t⊧𝖠1,fInit\models\mathsf{A}_{1},f, I​n​i​t⊧𝖠2Init\models\mathsf{A}_{2}, and 𝖠2⪯𝖠1\mathsf{A}_{2}\preceq\mathsf{A}_{1}, then I​n​i​t⊧𝖠2,fInit\models\mathsf{A}_{2},f.

5. Syndicate Framework

Before describing our algorithm, we fix templates for the set of possible invariants ℐ\mathcal{I} and possible ranking functions ℱ\mathcal{F}. The algorithm can be instantiated with any templates (which can be different for each loop in the program), provided they satisfy the computability assumptions described in Theorem 5.3. We assume that the set of all possible program states (𝖨𝗍𝗋𝗎𝖾\mathsf{I}_{\mathsf{true}}) is in ℐ\mathcal{I} and that ℐ\mathcal{I} is closed under intersection, i.e., if 𝖨1,𝖨2∈ℐ\mathsf{I}_{1},\mathsf{I}_{2}\in\mathcal{I} then 𝖨1∩𝖨2∈ℐ\mathsf{I}_{1}\cap\mathsf{I}_{2}\in\mathcal{I}. Let us also fix a program 𝖯\mathsf{P} and a set of initial states I​n​i​tInit. The goal is to synthesize ranking functions from ℱ\mathcal{F} and invariants from ℐ\mathcal{I} that demonstrate that every loop inside 𝖯\mathsf{P} terminates. In the following section, we describe an algorithm that is both sound and complete — ranking functions and invariants identified constitute a correct proof of termination, and if there is a proof of termination using invariants in ℐ\mathcal{I} and ranking functions from ℱ\mathcal{F} then the algorithm does succeed. We first establish such a result under assumptions about the sets ℐ\mathcal{I} and ℱ\mathcal{F} and some computability assumptions about sub-procedures of our main algorithm. We then present algorithms for the sub-procedures that satisfy the computability assumptions needed for the soundness and completeness result.

5.1. Algorithm State

Consider a situation where our algorithm is trying to prove the termination of a loop 𝖫=while ​β​ do ​𝖯1​ od\mathsf{L}=\texttt{while }\beta\texttt{ do }\mathsf{P}_{1}\texttt{ od} inside program 𝖯\mathsf{P}. Syndicate maintains an algorithm state which is used to guess a candidate ranking function, and also check its correctness. It then iteratively refines its state until convergence. The algorithm state has two components: (1) an annotated program 𝖠∈𝖠​(𝖯)\mathsf{A}\in\mathsf{A}(\mathsf{P}) such that I​n​i​t⊧𝖠Init\models\mathsf{A}; this can be easily initialized by labeling each loop in 𝖯\mathsf{P} with SS, the set of all program states, (2) a finite set 𝗍⊆S×S\mathsf{t}\subseteq S\times S such that for any correct annotation 𝖠′\mathsf{A}^{\prime} of 𝖯\mathsf{P}, 𝗍⊆𝗂𝖽𝖨′∩⁣⟦β⟧∘⟦𝖠′[𝖯1]⟧\mathsf{t}\subseteq\mathsf{id}_{\mathsf{I}^{\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}[\mathsf{P}_{1}]\rrbracket, where 𝖨′\mathsf{I}^{\prime} is the annotation of 𝖫\mathsf{L} in 𝖠′\mathsf{A}^{\prime}. Since the pairs in tt are in the semantics of the loop body 𝖯1\mathsf{P}_{1}, it can be used to guess a candidate ranking function from the set Π​(𝗍,ℱ)≜{f∈ℱ|∀(s,s′)∈𝗍,f​(s)≥0∧f​(s)−f​(s′)≥1}\Pi(\mathsf{t},\mathcal{F})\triangleq\{f\in\mathcal{F}\>|\>\forall(s,s^{\prime})\in\mathsf{t},f(s)\geq 0\wedge f(s)-f(s^{\prime})\geq 1\}, that contains all the functions that reduce and are bounded on the pairs in tt. Next, the annotated program can be used to check the validity of the guessed candidate ranking functions.

Refinement of the Algorithm State

𝖠\mathsf{A}𝖠′\mathsf{A}^{\prime}𝖠∗\mathsf{A}^{*}
Figure 2. Assume that 𝖠∗\mathsf{A}^{*} can prove the validity of ff. Since 𝖠′⪯𝖠\mathsf{A}^{\prime}\preceq\mathsf{A}, 𝖠\mathsf{A} can be refined to 𝖠′\mathsf{A}^{\prime}, which can also prove the validity of ff.

Checking the correctness of ff may lead to at least one of the following cases. (1) The identification of additional pairs of states (si,si′)∉t(s_{i},s^{\prime}_{i})\notin t over which every valid ranking function must decrease. We add these newly discovered pairs to the algorithm state, i.e., t′←t∪{(si,si′)}t^{\prime}\leftarrow t\cup\{(s_{i},s^{\prime}_{i})\}. As a consequence, Π​(𝗍′,ℱ)⊂Π​(𝗍,ℱ)\Pi(\mathsf{t}^{\prime},\mathcal{F})\subset\Pi(\mathsf{t},\mathcal{F}). (2) The refinement of the annotated program to 𝖠′\mathsf{A}^{\prime} such that 𝖠′≺𝖠\mathsf{A}^{\prime}\prec\mathsf{A}. Thus, the algorithm progresses either by eliminating additional potential ranking functions or constructing a more precise model for the semantics of the program by a progressive refinement of the annotations of 𝖯\mathsf{P}. An important observation at this point is that in our algorithm, we always refine the annotations of the 𝖯\mathsf{P}, i.e. the new annotation 𝖠′\mathsf{A}^{\prime} is always ⪯𝖠\preceq\mathsf{A}. In Lemma 5.1, we prove that if there exists an annotated program 𝖠∗\mathsf{A}^{*} which proves the validity of a ranking function ff, then there also exists an annotated program 𝖠′⪯𝖠\mathsf{A}^{\prime}\preceq\mathsf{A}, which can prove ff valid (Fig. 2). This means that by refining the program’s annotations, we narrow down the space of all possible annotations without eliminating the possibility of verifying the validity of any correct ranking function.

Lemma 5.0.

Let 𝖠,𝖠∗∈𝖠​(𝖯)\mathsf{A},\mathsf{A}^{*}\in\mathsf{A}(\mathsf{P}) and ff be a ranking function. If I​n​i​t⊧𝖠Init\models\mathsf{A} and I​n​i​t⊧𝖠∗,fInit\models\mathsf{A}^{*},f then ∃𝖠′⪯𝖠\exists\mathsf{A}^{\prime}\preceq\mathsf{A} and I​n​i​t⊧𝖠′,fInit\models\mathsf{A}^{\prime},f.

Proof.

Let 𝖠′=𝖠∧𝖠∗\mathsf{A}^{\prime}=\mathsf{A}\wedge\mathsf{A}^{*}. Clearly, 𝖠′⪯𝖠\mathsf{A}^{\prime}\preceq\mathsf{A}. It follows from Proposition 4.2 that I​n​i​t⊧𝖠′,fInit\models\mathsf{A}^{\prime},f. ∎

5.2. Detailed Algorithm

Syndicate (Algorithm 1) iteratively generates a candidate ranking function and then uses it to refine the algorithm state if the candidate ranking function is not valid. The function get_candidate (line 5) returns a ranking function from the set Π​(𝗍,ℱ)\Pi(\mathsf{t},\mathcal{F}) if one exists and returns 𝖿𝖺𝗅𝗌𝖾\mathsf{false} if Π​(𝗍,ℱ)\Pi(\mathsf{t},\mathcal{F}) is empty. The function check (line 10) returns 𝗍𝗋𝗎𝖾\mathsf{true} if I​n​i​t⊧𝖠,fInit\models\mathsf{A},f and 𝖿𝖺𝗅𝗌𝖾\mathsf{false} otherwise. We assume that if check fails, get_cex produces a counter-example (line 13). The counter-example is a pair of states (p,p′)(p,p^{\prime}) such that (a) (p,p′)∈⟦𝖠[𝖯1]⟧(p,p^{\prime})\in\llbracket\mathsf{A}[\mathsf{P}_{1}]\rrbracket, (b) p∈𝖨∩⟦β⟧p\in\mathsf{I}\cap\llbracket\beta\rrbracket, where 𝖨\mathsf{I} is the invariant labeling 𝖫\mathsf{L} in 𝖠\mathsf{A}, and (c) either f​(p)<0f(p)<0 or f​(p)−f​(p′)<1f(p)-f(p^{\prime})<1.

Algorithm 1 Syndicate

Inputs: 𝗍\mathsf{t} - Set of traces, 𝖠\mathsf{A} - Program annotated with the invariants (initialized with 𝖨𝗍𝗋𝗎𝖾\mathsf{I}_{\mathsf{true}})
Output: 𝗍𝗋𝗎𝖾\mathsf{true} if termination is proved, 𝖿𝖺𝗅𝗌𝖾\mathsf{false} otherwise

1:procedure find_ranking(𝗍,𝖠\mathsf{t},\mathsf{A})
2:     is_refined←𝖿𝖺𝗅𝗌𝖾\texttt{is\_refined}\leftarrow\mathsf{false}
3:     while 𝗍𝗋𝗎𝖾\mathsf{true} do
4:         if ¬is_refined\neg\texttt{is\_refined} then
5:              gen,f←get_candidate​(𝗍)\texttt{gen},f\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\_candidate}}}}(\mathsf{t})
6:              if ¬gen\neg\texttt{gen} then
7:                  return 𝖿𝖺𝗅𝗌𝖾\mathsf{false}
8:              end if
9:         end if
10:         if check​(f,𝖠)\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{check}}}}(f,\mathsf{A}) then
11:              return 𝗍𝗋𝗎𝖾\mathsf{true}
12:         end if
13:         (p,p′)←get_cex​(f,𝖠)(p,p^{\prime})\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\_cex}}}}(f,\mathsf{A})
14:         is_refined,𝖠,t←refine​(𝖠,(p,p′),t)\texttt{is\_refined},\;\mathsf{A},t\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),t)
15:         if ¬is_refined\neg\texttt{is\_refined} then
16:              𝗍←𝗍∪{(p,p′)}\mathsf{t}\leftarrow\mathsf{t}\cup\{(p,p^{\prime})\}
17:         end if
18:     end while
19:end procedure

If ff is not a valid ranking function for 𝖫\mathsf{L} then the counter-example (p,p′)(p,p^{\prime}) is used to refine the program state (line 14). The counter-example can be eliminated in one of two ways: (1) The invariants in 𝖠\mathsf{A} are refined so that pp is not an entry state of loop 𝖫\mathsf{L} or (p,p′)(p,p^{\prime}) is not in the semantics of the body 𝖯1\mathsf{P}_{1}, or (2) A new ranking function is synthesized that behaves correctly on the pair (p,p′)(p,p^{\prime}). The subroutine refine (line 14) tries to eliminate (p,p′)(p,p^{\prime}) by refining the invariants in 𝖠\mathsf{A}. The crucial property we require of refine is as follows.

  1. (1)

    If refine​(𝖠,(p,p′),𝗍)\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),\mathsf{t}) returns (𝗍𝗋𝗎𝖾,𝖠′,t′)(\mathsf{true},\mathsf{A}^{\prime},t^{\prime}) then it must be the case 𝖠′≺𝖠\mathsf{A}^{\prime}\prec\mathsf{A} and I​n​i​t⊧𝖠′Init\models\mathsf{A}^{\prime}.

  2. (2)

    If refine​(𝖠,(p,p′),𝗍)\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),\mathsf{t}) returns (𝖿𝖺𝗅𝗌𝖾,𝖠′,t′)(\mathsf{false},\mathsf{A}^{\prime},t^{\prime}) then 𝖠′=𝖠\mathsf{A}^{\prime}=\mathsf{A} and for every correct 𝖠′′\mathsf{A}^{\prime\prime} (i.e. I​n​i​t⊧𝖠′′Init\models\mathsf{A}^{\prime\prime}) with 𝖠′′≺𝖠\mathsf{A}^{\prime\prime}\prec\mathsf{A}, (p,p′)∈𝗂𝖽𝖨′′∩⁣⟦β⟧∘⟦𝖠′′[𝖯1]⟧(p,p^{\prime})\in\mathsf{id}_{\mathsf{I}^{\prime\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime\prime}[\mathsf{P}_{1}]\rrbracket where 𝖨′′\mathsf{I}^{\prime\prime} is the invariant labelling 𝖫\mathsf{L} in 𝖠′′\mathsf{A}^{\prime\prime}. In other words, (p,p′)(p,p^{\prime}) is in the semantics of the body of the loop 𝖫\mathsf{L} in every refinement of 𝖠\mathsf{A}.

In both of the above cases, t⊆t′⊆⟦𝖯1⟧t\subseteq t^{\prime}\subseteq\llbracket\mathsf{P}_{1}\rrbracket and 𝖽𝗈𝗆​(t′)⊆ℛ\mathsf{dom}(t^{\prime})\subseteq\mathcal{R}. Note that if refine is unable to refine (returns 𝖿𝖺𝗅𝗌𝖾\mathsf{false}), then by the definition of refine, for every 𝖠′′≺𝖠\mathsf{A}^{\prime\prime}\prec\mathsf{A}, (p,p′)(p,p^{\prime}) is in the semantics of the loop 𝖫\mathsf{L} captured by 𝖠′′\mathsf{A}^{\prime\prime}. The following lemma lifts this to all possible valid 𝖠′′\mathsf{A}^{\prime\prime} and proves that if refine returns 𝖿𝖺𝗅𝗌𝖾\mathsf{false}, it means that (p,p′)(p,p^{\prime}) is in the semantics of the loop 𝖫\mathsf{L} captured by all valid annotated programs (not limited to ≺𝖠\prec\mathsf{A}). So, we add (p,p′)(p,p^{\prime}) to 𝗍\mathsf{t} to get a new set 𝗍𝗇𝖾𝗐\mathsf{t}_{\mathsf{new}}. Note that 𝗍𝗇𝖾𝗐\mathsf{t}_{\mathsf{new}} continues to satisfy the property that we required of 𝗍\mathsf{t}.

Lemma 5.0.

Suppose refine​(𝖠,(p,p′),𝗍)\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),\mathsf{t}) returns (𝖿𝖺𝗅𝗌𝖾,𝖠,t′)(\mathsf{false},\mathsf{A},t^{\prime}). Consider any annotated program 𝖠′∈𝖠​(𝖯)\mathsf{A}^{\prime}\in\mathsf{A}(\mathsf{P}) such that I​n​i​t⊧𝖠′Init\models\mathsf{A}^{\prime}. Let 𝖨′\mathsf{I}^{\prime} be the annotation of 𝖫\mathsf{L} in 𝖠′\mathsf{A}^{\prime}. Then (p,p′)∈𝗂𝖽𝖨′∩⁣⟦β⟧∘⟦𝖠′[𝖯1]⟧(p,p^{\prime})\in\mathsf{id}_{\mathsf{I}^{\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}[\mathsf{P}_{1}]\rrbracket.

Proof.

Suppose the claim is not true, i.e., for some correct annotated program 𝖠′\mathsf{A}^{\prime}, (p,p′)∉𝗂𝖽𝖨′∩⁣⟦β⟧∘⟦𝖠′[𝖯1]⟧(p,p^{\prime})\not\in\mathsf{id}_{\mathsf{I}^{\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}[\mathsf{P}_{1}]\rrbracket. Consider the program 𝖠∧𝖠′≺𝖠\mathsf{A}\wedge\mathsf{A}^{\prime}\prec\mathsf{A}. By Lemma 5.1, 𝖠∧𝖠′\mathsf{A}\wedge\mathsf{A}^{\prime} is correct and (p,p′)(p,p^{\prime}) is not valid pair for the semantics of the loop body 𝖯1\mathsf{P}_{1}. In such a case refine must return 𝗍𝗋𝗎𝖾\mathsf{true} giving us the desired contradiction. ∎

By processing counter-example (p,p′)(p,p^{\prime}), our algorithm always makes progress. There are two cases to consider. If refine returns 𝗍𝗋𝗎𝖾\mathsf{true} then we have a new correct annotated program 𝖠′\mathsf{A}^{\prime} that refines 𝖠\mathsf{A}. On the other hand, if refine returns 𝖿𝖺𝗅𝗌𝖾\mathsf{false} then we have new set 𝗍𝗇𝖾𝗐\mathsf{t}_{\mathsf{new}} with the property that Π​(𝗍𝗇𝖾𝗐,ℱ)⊊Π​(𝗍,ℱ)\Pi(\mathsf{t}_{\mathsf{new}},\mathcal{F})\subsetneq\Pi(\mathsf{t},\mathcal{F}). This is because f∈Π​(𝗍,ℱ)∖Π​(𝗍𝗇𝖾𝗐,ℱ)f\in\Pi(\mathsf{t},\mathcal{F})\setminus\Pi(\mathsf{t}_{\mathsf{new}},\mathcal{F}) since ff is not a valid ranking function for the pair (p,p′)(p,p^{\prime}). Thus, in this case Π​(𝗍𝗇𝖾𝗐,ℱ)\Pi(\mathsf{t}_{\mathsf{new}},\mathcal{F}) has become smaller.

5.3. Soundess, Completeness, and Efficiency of Syndicate

Algorithm 1 can be shown to be sound and complete for proving the termination of loop 𝖫\mathsf{L} of 𝖯\mathsf{P}. In this context, soundness means that if our algorithm succeeds and returns a ranking function ff from ℱ\mathcal{F}, then there exists an invariant in ℐ\mathcal{I} that can prove that ff is a valid ranking function for 𝖫\mathsf{L}. Conversely, completeness means that if there is a function f∈ℱf\in\mathcal{F} and 𝖨∈ℐ\mathsf{I}\in\mathcal{I} such that ff can be proved valid using 𝖨\mathsf{I}, then Algorithm 1 will prove termination.

Theorem 5.3.

Suppose there exist complete procedures for the functions get_candidate, check, get_cex, and refine that satisfy the properties defined above. Further, suppose the set ℱ\mathcal{F} is finite, and ℐ\mathcal{I} is closed under intersection and has no infinite descending chains (w.r.t the subset relation). Then Algorithm 1 is a sound and complete method to prove the termination of loop 𝖫\mathsf{L} of 𝖯\mathsf{P}.

Proof Sketch.

The soundness of the algorithm follows from the semantics of get_candidate and check. Suppose there is a ranking function f∗f^{*} and an annotated program 𝖠∗\mathsf{A}^{*} such that 𝖠∗\mathsf{A}^{*} is a correct annotation of 𝖯\mathsf{P} and f∗f^{*} is a valid ranking function that proves the termination of 𝖫\mathsf{L}. Let (𝖠,𝗍)(\mathsf{A},\mathsf{t}) be the state of the algorithm at any point. Observe that because of the property that the algorithm maintains of 𝗍\mathsf{t}, we have f∗∈Π​(𝗍,ℱ)f^{*}\in\Pi(\mathsf{t},\mathcal{F}). By Lemma 5.1 there is a correct annotated program 𝖠′(=𝖠∧𝖠∗)⪯𝖠\mathsf{A}^{\prime}(=\mathsf{A}\wedge\mathsf{A}^{*})\preceq\mathsf{A} such that f∗f^{*} proves the termination of 𝖫\mathsf{L} in 𝖠′\mathsf{A}^{\prime}. Finally, the assumptions on ℐ\mathcal{I} and ℱ\mathcal{F} mean that Π​(𝗍,ℱ)\Pi(\mathsf{t},\mathcal{F}) and 𝖠↓={𝖠′|𝖠′⪯𝖠}\mathsf{A}\downarrow=\{\mathsf{A}^{\prime}\>|\>\mathsf{A}^{\prime}\preceq\mathsf{A}\} are both finite sets and hence there can only be finitely many steps of refinement. Thus Algorithm 1 will terminate with the right answer. ∎

Efficiency

Consider a meet semilattice (ℒℱ,⪯,∧)\mathcal{L}_{\mathcal{F}},\preceq,\wedge) induced by ℱ\mathcal{F} where each element is a set of ranking functions from ℱ\mathcal{F} and ⪯,∧\preceq,\wedge are defined by the set operations ⊆,∩\subseteq,\cap. In each refinement step, we either (1) add a pair of states to 𝗍\mathsf{t} creating 𝗍n​e​w\mathsf{t}_{new}, which in turn decreases the size of the set of ranking functions Π\Pi determined by the algorithm’s state, as Π​(𝗍n​e​w,ℱ)⊂Π​(𝗍,ℱ)\Pi(\mathsf{t}_{new},\mathcal{F})\subset\Pi(\mathsf{t},\mathcal{F}). The number of times this refinement can be performed is bounded by the depth of the semilattice ℒℱ\mathcal{L}_{\mathcal{F}}, or (2) we refine the current annotation 𝖠\mathsf{A} to 𝖠′\mathsf{A}^{\prime}, where 𝖠′≺𝖠\mathsf{A}^{\prime}\prec\mathsf{A}. This is bounded by the depth of the meet semilattice for the annotated programs ℒ𝖠\mathcal{L}_{\mathsf{A}}. This bounds the number of iterations of our algorithm to 𝖽𝖾𝗉𝗍𝗁​(ℒℱ)+𝖽𝖾𝗉𝗍𝗁​(ℒ𝖠)\mathsf{depth}(\mathcal{L}_{\mathcal{F}})+\mathsf{depth}(\mathcal{L}_{\mathsf{A}}). This worst-case bound is much better than the unguided search for invariants and ranking functions. A naive termination algorithm that searches for invariants and ranking functions independently would realize a worst-case bound of |ℒℱ|×|ℒ𝖠||\mathcal{L}_{\mathcal{F}}|\ \times\ |\mathcal{L}_{\mathsf{A}}|, where |⋅||\cdot| represents the number of elements in the lattice. Even a strategy that ensures refinement at each step of the algorithm, and hence a downward movement in their respective lattice, would have a worst-case bound of 𝖽𝖾𝗉𝗍𝗁​(ℒℱ)×𝖽𝖾𝗉𝗍𝗁​(ℒ𝖠)\mathsf{depth}(\mathcal{L}_{\mathcal{F}})\times\mathsf{depth}(\mathcal{L}_{\mathsf{A}}). Thus, we argue that Syndicate’s synergistic synthesis for invariants and ranking functions has significant merit. In Section 7, we show that Syndicate is better than the state-of-the-art termination analysis tools in terms of runtime analysis for non-trivial programs.

5.4. Detailed Subprocedures

Algorithm 2 Algorithm for Refine State

Inputs: Annotated program (𝖠\mathsf{A}), counter-example ((p,p′(p,p^{\prime}), reachable state pairs (tt)
Output: 𝗍𝗋𝗎𝖾\mathsf{true} or 𝖿𝖺𝗅𝗌𝖾\mathsf{false}, refined annotated program (𝖠′\mathsf{A}^{\prime}), additional reachable states pairs (tt)

1:procedure 𝗋𝖾𝖿𝗂𝗇𝖾\mathsf{refine}(𝖠,(p,p′),t\mathsf{A},(p,p^{\prime}),t)
2:     𝗂𝗇𝗏𝖼\mathsf{inv_{c}} = []
3:     𝖠′,gen←get_inv​(t,(p,p′),𝗂𝗇𝗏𝖼)\mathsf{A}^{\prime},\text{gen}\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\_inv}}}}(t,(p,p^{\prime}),\mathsf{inv_{c}})
4:     while gen do
5:         if check_inv​(𝖠′)\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{check\_inv}}}}(\mathsf{A}^{\prime}) then
6:              return 𝗍𝗋𝗎𝖾\mathsf{true}, 𝖠∧𝖠′\mathsf{A}\wedge\mathsf{A}^{\prime}, tt
7:         end if
8:         (c,c′),𝖿𝗈𝗋​_​𝗉𝗋𝖾←get_cex_inv​(𝖠′)(c,c^{\prime}),\mathsf{for\_pre}\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\_cex\_inv}}}}(\mathsf{A}^{\prime})
9:         if 𝖿𝗈𝗋​_​𝗉𝗋𝖾\mathsf{for\_pre} then
10:              t←t∪{(c,c′)}t\leftarrow t\cup\{(c,c^{\prime})\}
11:         else
12:              𝗂𝗇𝗏𝖼←𝗂𝗇𝗏𝖼∪{(c,c′)}\mathsf{inv_{c}}\leftarrow\mathsf{inv_{c}}\cup\{(c,c^{\prime})\}
13:         end if
14:         𝖠′,gen←get_inv​(t,(p,p′),𝗂𝗇𝗏𝖼)\mathsf{A}^{\prime},\text{gen}\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\_inv}}}}(t,(p,p^{\prime}),\mathsf{inv_{c}})
15:     end while
16:     return 𝖿𝖺𝗅𝗌𝖾\mathsf{false}, 𝖠\mathsf{A}, tt
17:end procedure

We describe procedures for get_candidate, check, get_cex, and refine that satisfy the assumptions needed for soundness and completeness of Algorithm 1. For these procedures, we use SMT queries to generate and check the soundness of ranking functions for a given loop. We can define ℱ\mathcal{F} as a finite template for ranking functions. For the function get_candidate, given tt, we can generate an SMT query encoding a symbolic ranking function in ℱ\mathcal{F} that satisfies the reducing and bounded conditions for all of the pairs of states in tt. Finding a satisfying assignment to this query is equivalent to finding a candidate ranking function and if there is no satisfying assignment, then there is no ranking function in ℱ\mathcal{F} that is valid for the under-approximation, tt, and, therefore, there is no ranking function in ℱ\mathcal{F} that is valid for the loop. This follows the semantics of get_candidate described in Section 5.2. For this function to be decidable, one must be able to describe the set of all ranking functions in ℱ\mathcal{F} and express the bounded and reducing conditions on these ranking functions in a decidable SMT theory. Some examples of templates that lead to the SMT queries being decidable are the set of linear functions over the program variables, the set of polynomial functions over the program variables using real-valued coefficients, and the set of lexicographic functions where each component is a polynomial function using real-valued coefficients.

We can also use an SMT query for a function that implements the semantics of both check and get_cex. check checks the validity of ff given 𝖠\mathsf{A}. First, we define variables representing the state at the start of one iteration of the loop, (x1,⋯,xj)(x_{1},\cdots,x_{j}), and add the condition (x1,⋯,xj)∈𝖨(x_{1},\cdots,x_{j})\in\mathsf{I} where 𝖨\mathsf{I} is the invariant of the loop we are analyzing, retrieved from 𝖠\mathsf{A}. Then, we encode the over-approximation of the loop body defined by 𝖠\mathsf{A} into the SMT query. For each loop in the body of the outer loop, we define new variables, (xi,1,⋯,xi,j)(x_{i,1},\cdots,x_{i,j}) to represent the states at the exit of each inner loop, adding the condition (xi,1,⋯,xi,j)∈𝖨i∩⟦¬βi⟧(x_{i,1},\cdots,x_{i,j})\in\mathsf{I}_{i}\cap\llbracket\neg\beta_{i}\rrbracket, where 𝖨i\mathsf{I}_{i} and βi\beta_{i} are the invariant and loop guard of the inner loop from 𝖠\mathsf{A}. We define variables representing the state at the end of the iteration, (x1′,⋯,xj′)(x^{\prime}_{1},\cdots,x^{\prime}_{j}), and set these variables equal to the output state of ⟦𝖠⟧\llbracket\mathsf{A}\rrbracket when the input state is (x1,⋯,xj)(x_{1},\cdots,x_{j}). Checking the validity of ff using 𝖠\mathsf{A} is reduced to determining the satisfiability of the formula: (f​(x1,⋯,xj)−f​(x1′,⋯,xj′)<1)∨(f​(x1,⋯,xj)<0)(f(x_{1},\cdots,x_{j})-f(x^{\prime}_{1},\cdots,x^{\prime}_{j})<1)\vee(f(x_{1},\cdots,x_{j})<0). If this formula is unsatisfiable, then we have proven the validity of ff because we have established that ff is bounded and reducing on the possible state of the loop. If this formula is unsatisfiable, we return 𝗍𝗋𝗎𝖾\mathsf{true}. Otherwise, we return 𝖿𝖺𝗅𝗌𝖾\mathsf{false}. In Algorithm 1, get_cex is only called when check returns 𝖿𝖺𝗅𝗌𝖾\mathsf{false}. In this case, from the SMT query in check, we have a satisfying assignment to (x1,⋯,xj)(x_{1},\cdots,x_{j}) and (x1′,⋯,x′​j)(x^{\prime}_{1},\cdots,x^{\prime}j). The counter-example, (p,p′)(p,p^{\prime}), returned by get_cex​(f,𝖠)\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\_cex}}}}(f,\mathsf{A}) is ((x1,⋯,xj),(x1′,⋯,xj′))((x_{1},\cdots,x_{j}),(x^{\prime}_{1},\cdots,x^{\prime}_{j})). For this algorithm to be decidable, the SMT encoding of the program has to fit into a decidable SMT theory.

We now describe an algorithm that implements the semantics of the refine function and follows the properties defined in Section 5.2. Since we defined check to define symbolic states,(xi,1,⋯,xi,j)(x_{i,1},\cdots,x_{i,j}), at the end of each inner loop, instead of only storing (p,p′)(p,p^{\prime}), check can store (p1,⋯,pm)(p_{1},\cdots,p_{m}), where p1=pp_{1}=p, pm=p′p_{m}=p^{\prime} and pi=(xi,1,⋯,xi,j)p_{i}=(x_{i,1},\cdots,x_{i,j}) for all i∈[1,m]i\in[1,m]. This sequence of states will be used to define refine, shown in Algorithm 2.

First, we define how the refine function works when considering a single loop, and then extend it to multiple loops, nested or sequential. When refining the invariant for a non-nested loop given a candidate ranking function, ff, and a counter-example, (p,p′)(p,p^{\prime}), for ff to be a valid ranking function, pp has to not be a reachable state the beginning of one iteration of the outer loop. In our algorithm state, for a non-nested loop, we have an annotated program with one invariant, 𝖨\mathsf{I}. First we try to refine 𝖨\mathsf{I} to 𝖨′\mathsf{I}^{\prime} s.t. 𝖨′⊆𝖨∖{p}\mathsf{I}^{\prime}\subseteq\mathsf{I}\setminus\{p\}. For this, we first try to find an invariant, 𝖨′′\mathsf{I}^{\prime\prime}, that is a valid invariant and excludes the state pp and if this is possible, we return 𝖨∩𝖨′′\mathsf{I}\cap\mathsf{I}^{\prime\prime}. Note that 𝖨∩𝖨′′∈ℐ\mathsf{I}\cap\mathsf{I}^{\prime\prime}\in\mathcal{I} because ℐ\mathcal{I} is closed under intersection and 𝖨∩𝖨′′⊆𝖨∖{p}\mathsf{I}\cap\mathsf{I}^{\prime\prime}\subseteq\mathsf{I}\setminus\{p\}. To find 𝖨′′\mathsf{I}^{\prime\prime}, we iteratively generate possible invariants and then check their validity until either we have found a valid invariant that excludes pp or proved that no such invariant exists. We show this procedure in Algorithm 2. In lines 3 and 14, we generate new possible invariants. In line 5, we check the validity of the invariant. In lines 9-13, based on the output of the validity check we update the information used to generate new invariants.

To generate a possible invariant that excludes pp, we want to generate a set from ℐ\mathcal{I} that excludes pp and includes the states we know are reachable, 𝖽𝗈𝗆​(t)\mathsf{dom}(t). After we generate a possible invariant, 𝖨1\mathsf{I}_{1}, we check whether it includes I​n​i​tInit and is inductive. If 𝖨1\mathsf{I}_{1} does not include I​n​i​tInit, we obtain a state, c∈I​n​i​tc\in Init, s.t. c∉𝖨1c\notin\mathsf{I}_{1}. When we generate the next possible invariant, 𝖨2\mathsf{I}_{2}, we add the condition c∈𝖨′′c\in\mathsf{I}^{\prime\prime}. This condition is added by adding (c,c′)(c,c^{\prime}) to tt. If, on the other hand, 𝖨′\mathsf{I}^{\prime} is not inductive, we obtain a counter-example, (c,c′)(c,c^{\prime}) s.t. c∈𝖨1∧c′∉𝖨1c\in\mathsf{I}_{1}\wedge c^{\prime}\notin\mathsf{I}_{1}. In this case, to ensure we generate a different possible invariant, 𝖨2\mathsf{I}_{2}, we add the condition c∈𝖨2⟹c′∈𝖨2c\in\mathsf{I}_{2}\implies c^{\prime}\in\mathsf{I}_{2}. Note that the conditions we add in each iteration of generating possible invariants are 𝗍𝗋𝗎𝖾\mathsf{true} for all valid invariants of a loop.

We use i​n​vcinv_{c} to represent the set of pairs of states we obtained as counter-examples in previous iterations of checking the validity of possible invariants. i​n​vcinv_{c} is initialized to {}\{\}. We use the following SMT queries to find a candidate for 𝖨′′\mathsf{I}^{\prime\prime} (get_inv), and check its correctness (check_inv) respectively.

(3) (p∉𝖨′′)∧(⋀(s,s′)∈ts∈𝖨′′)∧(⋀(s,s′)∈i​n​vcs∈𝖨′′⟹s′∈𝖨′′)\Big{(}p\notin\mathsf{I}^{\prime\prime}\Big{)}\wedge\Big{(}\bigwedge_{(s,s^{\prime})\in t}s\in\mathsf{I}^{\prime\prime}\Big{)}\wedge\Big{(}\bigwedge_{(s,s^{\prime})\in inv_{c}}s\in\mathsf{I}^{\prime\prime}\implies s^{\prime}\in\mathsf{I}^{\prime\prime}\Big{)}
(4) (s∈Init∧s∉𝖨′′)∨(s∈𝖨′′∧⟦𝖯⟧s∉I′′)\Big{(}s\in Init\wedge s\notin\mathsf{I}^{\prime\prime}\Big{)}\vee\Big{(}s\in\mathsf{I}^{\prime\prime}\wedge\llbracket\mathsf{P}\rrbracket s\notin I^{\prime\prime}\Big{)}

If the SMT query checking the validity of 𝖨′′\mathsf{I}^{\prime\prime} is satisfiable, get_cex_inv either returns a state (c,c′)(c,c^{\prime}), s.t. c∈I​n​i​t∧(c,c′)∉𝖨′′c\in Init\wedge(c,c^{\prime})\not\in\mathsf{I}^{\prime\prime} or returns a pair of states (c,c′)(c,c^{\prime}) where c∈𝖨′′∧c′∉I′′c\in\mathsf{I}^{\prime\prime}\wedge c^{\prime}\notin I^{\prime\prime}. In the former case, we add this state to tt (line 10). In the latter case, we add this state to i​n​vcinv_{c} (line 12). With updated tt and i​n​vcinv_{c}, we repeat the process of generating and checking a new possible invariant.

5.5. Multiple Loops

In the case of multiple loops, we need to find 𝖠′≺𝖠\mathsf{A}^{\prime}\prec\mathsf{A}, where 𝖠\mathsf{A} is the annotated loop program in our algorithm state. As discussed earlier, in this instantiation of our framework, check will return (p1,⋯,pm)(p_{1},\cdots,p_{m}) instead of only (p,p′)(p,p^{\prime}). So, we have counter-examples, pip_{i}, for each invariant, 𝖨i\mathsf{I}_{i}, in the program. For each invariant, we maintain the set, tit_{i} and i​n​vciinv_{c_{i}}. tit_{i} is initialized to the set of states after the loop associated with 𝖨i\mathsf{I}_{i} obtained for the initial program execution traces and i​n​vciinv_{c_{i}} is initialized to an empty set. We use an SMT query to generate a candidate invariants, 𝖨i′\mathsf{I}^{\prime}_{i} for all of the loops such that at least one of the loops in 𝖠\mathsf{A} that excludes the counter-example, pip_{i} associated with 𝖨i\mathsf{I}_{i}. Formally, we find a satisfying assignment to the constants in 𝖨i′\mathsf{I}^{\prime}_{i} such that

(5) ⋁i(¬pi∈𝖨i∧⋀(s,s′)∈tis∈𝖨i∧(⋀(s,s′)∈i​n​vcis∈𝖨i⟹s′∈𝖨i))\bigvee_{i}\Big{(}\neg p_{i}\in\mathsf{I}_{i}\wedge\bigwedge_{(s,s^{\prime})\in t_{i}}s\in\mathsf{I}_{i}\wedge(\bigwedge_{(s,s^{\prime})\in inv_{c_{i}}}s\in\mathsf{I}_{i}\implies s^{\prime}\in\mathsf{I}_{i})\Big{)}

Once we find candidate invariants for all of the loops such that for at least one of the loops, 𝖨i′\mathsf{I}^{\prime}_{i} excludes pip_{i}, we check the validity of the candidate invariants. This validity check is done the same way as in the single loop case, and the counter-examples are either added to tit_{i} or i​n​vciinv_{c_{i}} accordingly. We repeatedly generate candidates to refine at least one of the invariants until one is found or there does not exist any valid invariant for any of the loops that exclude the corresponding counter-example, pip_{i}. In the latter case, we have shown that there is a sequence of reachable states w.r.t. the corresponding invariant templates that transition from pp to p′p^{\prime}. Therefore, (p,p′)(p,p^{\prime}) is in the semantics of the body of the loop for every possible refinement of 𝖠\mathsf{A}. In this case, we return 𝖿𝖺𝗅𝗌𝖾\mathsf{false}.

For the SMT queries that generate candidate invariants, one must be able to describe the set of all invariants in ℐ\mathcal{I} and express whether an invariant includes a state in a decidable SMT theory. For the SMT queries that check the validity of invariants at a point in the program to be decidable, the SMT encoding of the program has to fit into a decidable SMT theory.

6. Implementation of Syndicate

6.1. Templates

Consider the set of all ranking functions of the form: ∑imax⁡(a0i+∑jaji​xj,0)\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x_{j},0), where aji∈ℤa^{i}_{j}\in\mathbb{Z} and xix_{i} are program variables. This includes linear ranking functions as well as more complicated ranking functions that can be useful for non-linear assignment statements and complicated loop guards. We can extend this template to include lexicographic ranking functions, ⟨e1,⋯,en⟩\langle e_{1},\cdots,e_{n}\rangle, where each eke_{k} is of the form ∑imax⁡(a0i+∑jaji​xj,0)\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x_{j},0) for some i,j,n∈ℤi,j,n\in\mathbb{Z}. Here jj is the number of variables in a program. Bounding the absolute sum of the coefficients ajia^{i}_{j} for each lexicographic component, eke_{k}, ensures that this expanded set of ranking functions satisfies the conditions in Theorem 5.3. There are two parameters when defining this template, ii and nn. We define T​(i,n)T(i,n), to be a template in this form with ii summands per lexicographic expression and nn lexicographic expressions. Our implementation supports ranking function templates T​(i,n)T(i,n) for any values of ii and nn. For an invariant template that satisfies the conditions in Theorem 5.3, we use sets of states that can be represented by a conjunction of linear constraints, of the form d0+∑jdj​xj≥0d_{0}+\sum_{j}d_{j}x_{j}\geq 0 where dj∈ℤd_{j}\in\mathbb{Z}. This template is closed under intersection and we again bound the absolute sum of the coefficients did_{i}, which ensures that there is no infinite descending chain. In this section, ℱ\mathcal{F} and ℐ\mathcal{I} will refer to this specific ranking function template and this specific invariant template respectively.

6.2. Implementation of Subprocedures

get_candidate - This function returns an element of the set Π​(𝗍,ℱ)\Pi(\mathsf{t},\mathcal{F}). Since every function in ℱ\mathcal{F} is bounded below by 0, this problem reduces to finding a function f∈ℱf\in\mathcal{F} that reduces on all of the pairs of states in 𝗍\mathsf{t}. We can accomplish this by solving the following SMT query:

⋀(s,s′)∈𝗍((∑imax⁡(a0i+∑jaji​xj,0))−(∑imax⁡(a0i+∑jaji​xj′,0))≥1)\displaystyle\bigwedge_{(s,s^{\prime})\in\mathsf{t}}\Big{(}\big{(}\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x_{j},0)\big{)}-\big{(}\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x^{\prime}_{j},0)\big{)}\geq 1\Big{)}

Here, s=(x0,⋯​xj)s=(x_{0},\cdots x_{j}) represents a program state with concrete valuations of all program variables, and ajia^{i}_{j} are variables representing the coefficients of the ranking function. Note that having a large under-approximation, 𝗍\mathsf{t}, reduces the remaining size of the search space of ranking functions, Π​(𝗍,ℱ)\Pi(\mathsf{t},\mathcal{F}). However, this increases the size of the SMT query to generate a candidate ranking function. To manage this tradeoff, we introduce an optimization where we use a smaller set, 𝗍s\mathsf{t}_{s} s.t. 𝗍s⊂𝗍\mathsf{t}_{s}\subset\mathsf{t}, generate the candidate using 𝗍s\mathsf{t}_{s} and then check the generated candidate,ff, against the rest of the pairs of states in 𝗍\mathsf{t}. As soon as we find one element of 𝗍\mathsf{t} for which the ranking function does not decrease, we add it to 𝗍s\mathsf{t}_{s} and query the SMT again. We repeat this process till we have found a function in Π​(𝗍,ℱ)\Pi(\mathsf{t},\mathcal{F}) or the SMT query is unsatisfiable, meaning Π​(𝗍,ℱ)\Pi(\mathsf{t},\mathcal{F}) is empty.

check - This function takes as input ff and 𝖠\mathsf{A}. As discussed in Section 5.4, using the over-approximation of the loop body defined by ⟦𝖠⟧\llbracket\mathsf{A}\rrbracket, we define variables representing the state at the start of one iteration, (x1,⋯,xj)(x_{1},\cdots,x_{j}), the end of the iteration, (x1′,⋯,xj′)(x^{\prime}_{1},\cdots,x^{\prime}_{j}), and at the exit of each loop within the body of the outer loop, (x1,j,⋯,xi,j)(x_{1,j},\cdots,x_{i,j}). Then, we determine the satisfiability of the formula: f​((x1,⋯,xj))−f​((x1′,⋯,xj′))<1f((x_{1},\cdots,x_{j}))-f((x^{\prime}_{1},\cdots,x^{\prime}_{j}))<1. If this formula is unsatisfiable, then we have proven the validity of ff because we have already established that ff is bounded. If this formula is satisfiable, then the algorithm continues to refine either 𝖠\mathsf{A} or 𝗍\mathsf{t}.

get_cex - From the SMT query in check, we have found a satisfying assignment to (x1,⋯,xn)(x_{1},\cdots,x_{n}) and (x1′,⋯,xn′)(x^{\prime}_{1},\cdots,x^{\prime}_{n}). get_cex​(f,𝖠)\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\_cex}}}}(f,\mathsf{A}) returns the counter-example (p,p′)(p,p^{\prime}), where p=(x1,⋯,xn)p=(x_{1},\cdots,x_{n}) and p′=(x1′,⋯,xn′)p^{\prime}=(x^{\prime}_{1},\cdots,x^{\prime}_{n}). In our implementation, since we defined check to define variables, (x1,j,⋯,xn,j)(x_{1,j},\cdots,x_{n,j}), for the states at the end of each inner loop, instead of only returning (p,p′)(p,p^{\prime}), this function can return (p1,⋯,pm)(p_{1},\cdots,p_{m}), where p1=pp_{1}=p, pm=p′p_{m}=p^{\prime} and pi=(x1,j,⋯,xi,j)p_{i}=(x_{1,j},\cdots,x_{i,j}) for all i∈[1,m]i\in[1,m]. This sequence of states will be used to define refine to satisfy the properties defined in Section 5.

refine - As described in Section 5.4, when considering a program with one loop, we use Equations 3 and  4 to generate and check the validity of candidate invariants that exclude (p1,⋯,pm)(p_{1},\cdots,p_{m}) from the over-approximation of the transition relation of the loop. When considering multiple loops, since Equation 5 can be a large SMT query and is often not required to find a useful invariant, we try to refine the invariants for the loops in individual SMT queries to exclude the state pip_{i} from 𝖨i\mathsf{I}_{i}. If we cannot refine the invariants of any of the loops to exclude the corresponding counter-example, we assume that the states (p1,⋯,pm)(p_{1},\cdots,p_{m}) are reachable. This may not be true, because there could be a way to refine multiple invariants simultaneously to exclude a non-empty subset of the states (p1,⋯,pm)(p_{1},\cdots,p_{m}). Since (p,p′)(p,p^{\prime}) may be not be in the exact transition relation of the loop, instead of adding (p,p′)(p,p^{\prime}) to 𝗍\mathsf{t} we add it to a new set, 𝗍?\mathsf{t}^{?}. 𝗍?\mathsf{t}^{?} contains pairs of states for which we are unsure whether or not they are elements of ⟦𝖯⟧\llbracket\mathsf{P}\rrbracket. Whenever we refine an invariant for any loop in the program, we check whether the current annotated program, 𝖠\mathsf{A}, can prove that any states in 𝗍?\mathsf{t}^{?} are unreachable. If so, we remove those states from 𝗍?\mathsf{t}^{?}. When generating candidate ranking functions, instead of using 𝗍\mathsf{t}, we use 𝗍∪𝗍?\mathsf{t}\cup\mathsf{t}^{?}. So, the generate candidate phase changes to output a function, f∈ℱf\in\mathcal{F} that decreases and is bounded on all states in 𝗍∪𝗍?\mathsf{t}\cup\mathsf{t}^{?}. When no candidate ranking function is found, the algorithm terminates. Since 𝗍?\mathsf{t}^{?} may contain unreachable pairs of states, this algorithm can terminate without finding a valid ranking function even if one exists in ℱ\mathcal{F} that can be proved by an annotated program that has invariants in ℐ\mathcal{I}. The use of 𝗍?\mathsf{t}^{?} makes our implementation of the algorithm described in Section 5 incomplete. We further introduce some approximations in our implementation, by limiting the number of iterations of generating candidate invariants within the refine procedure and limiting the number of times we call refine without changing our candidate ranking function. When these approximations are used, the counter-examples from checking the validity of the ranking functions, (p,p′)(p,p^{\prime}), are added to 𝗍?\mathsf{t}^{?} instead of 𝗍\mathsf{t}.

7. Evaluation

We implement Syndicate in Python. As described in Section 6.1, for the template of invariants, we use a set of linear inequalities, specifically of the form of d0+∑dj​xj≥0d_{0}+\sum d_{j}x_{j}\geq 0, where dj∈ℤd_{j}\in\mathbb{Z}. For ranking functions, recall that we defined T​(i,n)T(i,n) to be a template with ii summands per lexicographic expression and nn lexicographic expressions. For our evaluation, we consider 5 templates with different values of i,ni,n, i.e., ℱ1=T​(1,1),ℱ2=T​(1,2),ℱ3=T​(1,3),ℱ4=T​(2,1),and​ℱ5=T​(2,2)\mathcal{F}_{1}=T(1,1),\;\mathcal{F}_{2}=T(1,2),\;\mathcal{F}_{3}=T(1,3),\;\mathcal{F}_{4}=T(2,1),\text{and}\;\mathcal{F}_{5}=T(2,2) Further, for all our experiments, we use 200 randomly generated initial traces. Syndicate expects Java programs as inputs and returns a ranking function and the corresponding loop invariants if it proves termination. We use Z3-Java API to check the validity of the ranking functions and the loop invariants. All experiments are run on a 2.50 GHz 16 core 11th Gen Intel i9-11900H CPU with a main memory of 64 GB. For all our tests, we use a timeout of 120 s. When computing the average time, we use the time taken to be 120 seconds for instances that timeout.

Benchmarks

We collect 168 challenging programs as benchmarks from the Term-crafted set of SV-COMP (Beyer, 2020), the Aprove_09 set from TermComp (Giesl et al., 2019), and ν\nuTerm-advantage from ν\nuTerm (Giacobbe et al., 2022). These benchmarks contain integer programs, with linear and non-linear assignments and loop guards, non-determinism, nested loops of maximum depth 3, and sequential loops. Except for random number generators, our implementation currently does not support function calls. However, the theory can be directly extended to support function calls by inlining them. The programs were originally in C but were also translated to Java by  (Giacobbe et al., 2022). The experiments for Syndicate and ν\nuTerm are run on the Java version while the experiments for Aprove, Ultimate, and DynamiTe are run on the equivalent C benchmarks.

7.1. Comparison with State-of-the-art Termination Analysis Tools

#\# Proved Avg. Time (s)
Syndicate 151 15.96
Ultimate 144 23.69
Aprove 142 22.31
DynamiTe 126 53.04
(a) Total number of benchmarks - 168
#\# Proved Avg. Time (s)
Syndicate 104 27.55
ν\nuTerm 95 33.13
(b) Total number of benchmarks - 128
Table 1. Total number of benchmarks proved and the average time for state-of-the-art termination analysis algorithms using a timeout of 2 minutes. Syndicate takes 32.6% less average time than Ultimate, 28.5% less than Aprove, 69.9% less than DynamiTe, and 16.8% less than ν\nuTerm.

We compare Syndicate against the following state-of-the-art tools for termination analysis.

  1. (1)

    Ultimate (Heizmann et al., 2014) decomposes programs into smaller sub-programs and constructs ranking functions for these sub-programs. After finding each ranking function, it checks whether the current set of sub-programs captures the behavior of the entire loop.

  2. (2)

    Aprove (Giesl et al., 2017) is an ensemble of several proof techniques, including termination proofs through reduction orders and dependency pairs.

  3. (3)

    DynamiTe (Le et al., 2020) tries to prove the non-termination of programs by finding recurrent sets, failing which it generates a counter-example that is then used to find candidate ranking functions. To finally prove termination, the synthesis of invariants is outsourced to an external invariant synthesis algorithm, DIG (Nguyen et al., 2014).

  4. (4)

    ν{\nu}Term (Giacobbe et al., 2022) trains a neural network from randomly generated traces to maximize the difference between the output of two consecutive states. The trained model is then treated as a candidate ranking function.

Refer to caption
Figure 3. Percentage of benchmarks proved terminating with growing running time. Syndicate is the overall best, except for easier benchmarks as it takes extra time to generate the initial 200 traces.
Refer to caption
Figure 4. No. of benchmarks proved terminating by Syndicate but not by the existing tool and vice-versa. The total number of benchmarks used is 128 for comparison with ν\nuTerm and 168 for all others.

For comparison to the above tools, Syndicate tests for the termination of a given benchmark using all 55 templates (ℱi\mathcal{F}_{i}) in parallel and stops as soon as one of the templates proves the termination. Note that all the existing tools also have a parallel implementation. In Table 1(a), we present the total number of benchmarks that each tool could prove and the average time taken to run the tools on a benchmark. The efficacy of Syndicate is demonstrated by the fact that it proves the most number of benchmarks and takes the least amount of average time. It is noteworthy that although state-of-the-art tools like Aprove employ an ensemble of several methods to prove termination, Syndicate surpasses them by relying solely on ranking functions to argue for program termination. Further, ν\nuTerm cannot handle the benchmarks with sequential loops or calls to random number generators and thus supports only a subset of the total benchmarks. So, we compare against ν\nuTerm in Table 1(b) on 128 benchmarks. Note that we can exactly match the template of ranking functions used by ν\nuTerm. So, for this experiment, we fix the template both for ν\nuTerm and Syndicate to ℱ4\mathcal{F}_{4}. ν\nuTerm uses 1000 initial traces for best baseline performance.

In Fig. 4, we show a cactus plot where the y-axis shows the percentage of total benchmarks proved terminating within the time on the x-axis. The x-axis is in the log scale. Syndicate achieves the overall fastest average running time compared to all other tools with minimal timeouts and leads on the cactus plot. In the initial 2.2s of the plot, Aprove is better than Syndicate. This is because Syndicate incurs a fixed cost since it uses program traces to generate candidate ranking functions. On the other hand, Aprove is a collection of several termination analysis techniques, due to which it can solve the easy benchmarks quickly. However, Syndicate surpasses Aprove in the long run and solves relatively more challenging benchmarks faster. In Fig. 4, we present the number of benchmarks that Syndicate could prove terminating, but the other tools could not, and also the number of benchmarks the existing tools could prove terminating, and Syndicate could not within the timeout limit. Syndicate can prove termination for significantly more benchmarks as compared to each of the existing tools. This highlights the distinct advantages and capabilities of Syndicate’s synergistic approach. Note that the comparison with ν\nuTerm is only using 128 benchmarks.

7.2. Case Studies

⬇
1 int x = y + 42;
2 while (x >= 0) {
3 y = 2 * y - x;
4 x = (y + x) / 2;
5 }
(a) Not proved by Aprove and Ultimate
⬇
1 int a = 0, b = 0;
2 while (a * b <= n || a * b <= m) {
3 a = a + 1;
4 b = b + 1;
5 }
(b) Not proved by any of Aprove, Ultimate, DynamiTe, and ν\nu-Term
Figure 5. Benchmarks for Case Studies proved terminating by Syndicate.

To shed more light on the efficacy of Syndicate, we discuss two non-trivial programs from our benchmarks where some of the existing tools fail to prove termination within the timeout while Syndicate succeeds in just 1.8s and 5.4s respectively. Specifically, we compare more qualitatively against DynamiTe and ν\nuTerm, which most closely resemble parts of Syndicate. Consider the program in Fig 5(a). To prove its termination, one tries to prove that xx reduces in successive iterations, which is not trivial. A non-trivial algebraic rewriting of the assignment expressions in lines 4 and 5 reveals that both xx and yy decrease by the value x−yx-y computed at the beginning of the iteration in each iteration. Furthermore, one needs an invariant at least as strong as x−y>0x-y>0 to show that xx always reduces. Unlike some other termination analysis tools, Syndicate does not rely on algebraic rewriting to infer the ranking functions and invariants. Instead, it uses traces to generate candidates and subsequently uses and SMT solver to verify its validity. Syndicate solves it in just 1.8s owing to its synergistic search for a termination argument and results in f∗≡max⁡(x+1,0)f^{*}\equiv\max(x+1,0) and 𝖨∗≡x−y≥1\mathsf{I}^{*}\equiv x-y\geq 1. Note that DynamiTe, which also relies on traces to come up with candidate ranking functions, is 5×\times slower and takes 11.9s to solve the problem. This is possibly because the invariant generation in DynamiTe is outsourced to DIG but does not explicitly guide the invariant search. Invariants other than 𝖨∗\mathsf{I}^{*} (like x−y≥42x-y\geq 42 or even stronger) may also prove the validity of f∗f^{*} but a naive unguided search for invariants results in longer runtime. Further, ν\nuTerm can also prove the termination in 2.56s, but its reliance on heuristically guessed invariants is not generalizable.

Similarly, Fig. 5(b) shows another non-trivial example consisting of non-linear expressions and disjunctive boolean guards, for which none of the existing tools used in our experiments could prove termination. Syndicate, however, generates a valid lexicographic ranking function ⟨max⁡(n−2​m+a−4​b+1,0),max⁡(m+a−2​b+6,0)⟩\langle\max(n-2m+a-4b+1,0),\max(m+a-2b+6,0)\rangle and loop invariant a≥ba\geq b that proves that the generated ranking function is valid in just 5.4s. Notably, even DynamiTe, which also uses trace-based methods to create ranking functions, fails to verify the termination even on increasing the timeout to 5 minutes. Our experiments with the invariant generation engine of DynamiTe (DIG) indicate that it takes a long time to produce invariants that are useful for proving the validity of the generated ranking functions. Further, even though there is a valid ranking function in the template used by ν\nuTerm, it fails to find it because of its inability to guess the required invariants. These examples demonstrate that a synergistic search can increase the number of benchmarks that can be proved terminating and also significantly reduce the analysis runtime by finding ranking functions from traces and by guiding the search for invariants just strong enough to prove it.

7.3. Ablation Studies

Refer to caption
(a) B-synergy1 and B-synergy2
Refer to caption
(b) B-combined
Figure 6. Percentage of benchmarks proved terminating with growing running time. Fig  6(a) uses 168 benchmarks and Fig  6(b) uses 153 benchmarks.
Refer to caption
(a) Syndicate vs B-synergy1
Refer to caption
(b) Syndicate vs B-synergy2
Figure 7. No. of benchmarks proved terminating by Syndicate but not by the baselines out of 168 benchmarks.

As highlighted in the introduction, we show that the two-way synergy used in Syndicate (invariant guiding the ranking function and vice-versa) is better than either one of them individually in terms of the number of proved benchmarks and the average runtime. We also show that the synergistic technique significantly outperforms searching for the ranking function and the invariant using a single query. The following experiments also show that the benefit of the synergy is independent of the exact instantiation of the template for ranking functions. For this, we implemented 3 baselines - B-synergy1, B-synergy2, and B-combined. First, B-synergy1 does not use the counter-examples from checking the validity of candidate invariants to guide the generation of new candidate ranking functions. This demonstrates the effect of having only the ranking function guide the invariant search. Second, B-synergy2 does not use the counter-examples from checking the validity of candidate ranking functions to guide the generation of new candidate invariants. This demonstrates the effect of having only the invariant guide the ranking function search. Third, B-combined searches for both ranking function and invariant with a single monolithic query. In the following experiments, the baselines use the same template for invariants as Syndicate. B-synergy1 and B-synergy2 are instantiated with the 5 ranking function templates ℱi\mathcal{F}_{i} described in Section 7. B-combined is only instantiated with ℱ1\mathcal{F}_{1} because ℱ1\mathcal{F}_{1} is the simplest template and B-combined does not scale well even with ℱ1\mathcal{F}_{1}.

Template Syndicate B-synergy1 B-synergy2
ℱ1\mathcal{F}_{1} 94 85 83
ℱ2\mathcal{F}_{2} 142 134 128
ℱ3\mathcal{F}_{3} 146 138 137
ℱ4\mathcal{F}_{4} 121 112 109
ℱ5\mathcal{F}_{5} 131 127 110
Table 2. The number of benchmarks out of 168 proved by Syndicate and baselines for different templates.

In Fig. 6(a), we show the percentage benchmarks proved with growing time for Syndicate, B-synergy1, and B-synergy2 in the case of template ℱ2\mathcal{F}_{2}. We can see that both baselines perform worse than Syndicate, indicating that using both the counter-examples from the invariant search and the counter-examples from the ranking function search to guide each other increases the number of benchmarks proved. The graphs for other templates are similar and can be found in Appendix C. In Table 2, we show the numbers of benchmarks proved by Syndicate and B-synergy1 and B-synergy2 using each template. There is up to 8% improvement over B-synergy1 and up to 19% improvement over B-synergy2. In Figs. 7(a),  7(b), we show the number of benchmarks that are uniquely solved by B-synergy(i) as compared to Syndicate. We can see that Syndicate is significantly better than both the baselines. We observe that in a few benchmarks, the baselines are better than Syndicate due to the non-determinism involved in guessing the candidates. In Fig. 6(b), we compare the Syndicate to B-combined, using ℱ1\mathcal{F}_{1} for both. Our implementation of B-combined only handles non-nested loops, so we use 153 benchmarks to evaluate B-combined. B-combined can solve only 31 of the total benchmarks. It solves these quickly because of less number of iterations needed but times out on relatively more complicated benchmarks because there is a large search space for the query. This shows that such a strategy cannot scale as the complexity of the benchmarks grows.

8. Related Works

Termination Analysis. Numerous techniques have been designed to reason about termination (Giacobbe et al., 2022; Urban et al., 2016; Cook et al., 2006; Xie et al., 2017; Le et al., 2020; Gonnord et al., 2015; Podelski and Rybalchenko, 2004; Bradley et al., 2005b) and non-termination (Le et al., 2020; Heizmann et al., 2014; Velroyen and Rümmer, 2008; Han and He, 2023; Chen et al., 2014) of programs. Synthesizing ranking functions is one well-established way of proving termination. As discussed in Section 1, there are techniques that separate the search for a valid ranking function and an invariant strong enough to prove it (Urban et al., 2016; Giacobbe et al., 2022; Le et al., 2020; Cook et al., 2006). These can handle a wide variety of programs but do not provide completeness guarantees. There are techniques that provide completeness guarantees but handle a restricted class of programs(Gonnord et al., 2015; Podelski and Rybalchenko, 2004; Bradley et al., 2005a; Heizmann et al., 2014). For example, (Podelski and Rybalchenko, 2004; Bradley et al., 2005a) propose complete methods to find linear ranking functions and linear invariants to prove the termination of linear programs. There are also techniques that provide completeness guarantees and handle complex programs (Unno et al., 2021, 2023), but these techniques encode an over-approximation of the reachable states and ranking functions in a single formula.  (Unno et al., 2023) is more scalable, but it relies on information from searching for non-termination arguments to make the search for termination arguments scalable. Syndicate focuses only on termination and proves termination by synthesizing ranking functions and invariants in different sub-routines that exchange important information. It can handle a wide variety of programs and also offers relative completeness guarantees while maintaining efficiency.

Guided search for invariants. Several previous works (Nguyen et al., 2014, 2022) have focused on identifying loop invariants. These works, however, aim to discover loop invariants without being specifically guided by a particular property. It has been established (Furia and Meyer, 2010; Galeotti et al., 2015; Miltner et al., 2020; Padon et al., 2022; Garg et al., 2014) that proving properties does not always need the identification of the strongest invariants. Instead, it is often more efficient to search for invariants that specifically contribute to proving the desired property. (Welp and Kuehlmann, 2014) leverages the concept of Property Directed Reachability (Bradley, 2011) to infer invariants that are directed toward achieving the goal of proving the input verification condition. (Miltner et al., 2020) proposes a counterexample-driven algorithm for inferring invariants sufficient to imply some desired specifications. Our search for invariant is also guided by a goal, which is to prove the validity of a ranking function. But we do not have a target ranking function. So, we synergistically guide the search for invariants and ranking functions.

Counter-example guided learning. Many frameworks like CEGIS (Solar-Lezama et al., 2008; Clarke et al., 2000; Gupta et al., 2020; Preiner et al., 2017) work on the methodology of using counter-examples to guide their search for specific candidates (programs, abstractions etc.) that satisfy a fixed property. Our approach, while similar, poses a greater challenge as we are simultaneously searching for both a valid ranking function and an invariant that can prove it in seperate CEGIS loops that guide each other.

9. Conclusion

We developed a general recipe called Syndicate for automated termination analysis based on a synergistic synthesis of invariants and ranking functions. Syndicate can be instantiated with different templates for invariants and ranking functions, is relatively complete, and can handle complex programs. We provided a specific instantiation of Syndicate where invariants are represented as linear inequalities and ranking functions are lexicographic expressions, with sums of max terms. We empirically showed that this specific instantiation can prove the termination of more benchmarks than state-of-the-art termination analysis tools and in a faster time. We leave instantiation of Syndicate with more complex templates and the development of an algorithm to automatically discover suitable templates for a given program as future works.

References

  • (1)
  • Beyer (2020) Dirk Beyer. 2020. Advances in Automatic Software Verification: SV-COMP 2020. In Tools and Algorithms for the Construction and Analysis of Systems, Armin Biere and David Parker (Eds.). Springer International Publishing, Cham, 347–367.
  • Bradley (2011) Aaron R. Bradley. 2011. SAT-Based Model Checking without Unrolling. In Verification, Model Checking, and Abstract Interpretation, Ranjit Jhala and David Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 70–87.
  • Bradley et al. (2005a) Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005a. Linear Ranking with Reachability. In Computer Aided Verification, Kousha Etessami and Sriram K. Rajamani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 491–504.
  • Bradley et al. (2005b) Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005b. Termination of Polynomial Programs. In Verification, Model Checking, and Abstract Interpretation, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 113–129.
  • Chen et al. (2014) Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter O’Hearn. 2014. Proving Nontermination via Safety. In Tools and Algorithms for the Construction and Analysis of Systems, Erika Ábrahám and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 156–171.
  • Clarke et al. (2000) Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. In Computer Aided Verification, E. Allen Emerson and Aravinda Prasad Sistla (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 154–169.
  • Cook et al. (2006) Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination Proofs for Systems Code. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (Ottawa, Ontario, Canada) (PLDI ’06). Association for Computing Machinery, New York, NY, USA, 415–426. https://doi.org/10.1145/1133981.1134029
  • de Moura and Bjørner (2008) Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS (Lecture Notes in Computer Science, Vol. 4963). Springer, 337–340.
  • Furia and Meyer (2010) Carlo Alberto Furia and Bertrand Meyer. 2010. Inferring Loop Invariants Using Postconditions. Springer Berlin Heidelberg, Berlin, Heidelberg, 277–300. https://doi.org/10.1007/978-3-642-15025-8_15
  • Galeotti et al. (2015) Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller. 2015. Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking. IEEE Transactions on Software Engineering 41, 10 (2015), 1019–1037. https://doi.org/10.1109/TSE.2015.2431688
  • Garg et al. (2014) Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. 2014. ICE: A Robust Framework for Learning Invariants. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 69–87.
  • Giacobbe et al. (2022) Mirco Giacobbe, Daniel Kroening, and Julian Parsert. 2022. Neural Termination Analysis. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (Singapore, Singapore) (ESEC/FSE 2022). Association for Computing Machinery, New York, NY, USA, 633–645. https://doi.org/10.1145/3540250.3549120
  • Giesl et al. (2017) Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. 2017. Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 58, 1 (jan 2017), 3–31. https://doi.org/10.1007/s10817-016-9388-y
  • Giesl et al. (2019) Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. 2019. The Termination and Complexity Competition. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 156–166.
  • Gonnord et al. (2015) Laure Gonnord, David Monniaux, and Gabriel Radanne. 2015. Synthesis of Ranking Functions Using Extremal Counterexamples. SIGPLAN Not. 50, 6 (jun 2015), 608–618. https://doi.org/10.1145/2813885.2737976
  • Gupta et al. (2020) Shubhani Gupta, Abhishek Rose, and Sorav Bansal. 2020. Counterexample-Guided Correlation Algorithm for Translation Validation. Proc. ACM Program. Lang. 4, OOPSLA, Article 221 (nov 2020), 29 pages. https://doi.org/10.1145/3428289
  • Han and He (2023) Zhilei Han and Fei He. 2023. Data-driven Recurrent Set Learning For Non-termination Analysis. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 1303–1315. https://doi.org/10.1109/ICSE48619.2023.00115
  • Heizmann et al. (2014) Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs. https://doi.org/10.1007/978-3-319-08867-9_53
  • Le et al. (2020) Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, and ThanhVu Nguyen. 2020. DynamiTe: Dynamic Termination and Non-Termination Proofs. Proc. ACM Program. Lang. 4, OOPSLA, Article 189 (nov 2020), 30 pages. https://doi.org/10.1145/3428257
  • Miltner et al. (2020) Anders Miltner, Saswat Padhi, Todd Millstein, and David Walker. 2020. Data-Driven Inference of Representation Invariants. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK) (PLDI 2020). Association for Computing Machinery, New York, NY, USA, 1–15. https://doi.org/10.1145/3385412.3385967
  • Nguyen et al. (2014) Thanhvu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. 2014. DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Trans. Softw. Eng. Methodol. 23, 4, Article 30 (sep 2014), 30 pages. https://doi.org/10.1145/2556782
  • Nguyen et al. (2022) ThanhVu Nguyen, KimHao Nguyen, and Hai Duong. 2022. SymInfer: Inferring Numerical Invariants using Symbolic States. In 2022 IEEE/ACM 44th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). 197–201. https://doi.org/10.1145/3510454.3516833
  • Padon et al. (2022) Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken. 2022. Induction Duality: Primal-Dual Search for Invariants. Proc. ACM Program. Lang. 6, POPL, Article 50 (jan 2022), 29 pages. https://doi.org/10.1145/3498712
  • Podelski and Rybalchenko (2004) Andreas Podelski and Andrey Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. In Verification, Model Checking, and Abstract Interpretation, Bernhard Steffen and Giorgio Levi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 239–251.
  • Preiner et al. (2017) Mathias Preiner, Aina Niemetz, and Armin Biere. 2017. Counterexample-Guided Model Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 264–280.
  • Solar-Lezama et al. (2008) Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. 2008. Sketching Concurrent Data Structures. SIGPLAN Not. 43, 6 (jun 2008), 136–148. https://doi.org/10.1145/1379022.1375599
  • Unno et al. (2023) Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. 2023. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. Proc. ACM Program. Lang. 7, POPL, Article 72 (jan 2023), 30 pages. https://doi.org/10.1145/3571265
  • Unno et al. (2021) Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham, 742–766.
  • Urban et al. (2016) Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016. Synthesizing Ranking Functions from Bits and Pieces. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-François Raskin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 54–70.
  • Velroyen and Rümmer (2008) Helga Velroyen and Philipp Rümmer. 2008. Non-termination Checking for Imperative Programs. In Tests and Proofs, Bernhard Beckert and Reiner Hähnle (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 154–170.
  • Welp and Kuehlmann (2014) Tobias Welp and Andreas Kuehlmann. 2014. Property directed invariant refinement for program verification. In 2014 Design, Automation & Test in Europe Conference & Exhibition (DATE). 1–6. https://doi.org/10.7873/DATE.2014.127
  • Xie et al. (2017) Xiaofei Xie, Bihuan Chen, Liang Zou, Shang-Wei Lin, Yang Liu, and Xiaohong Li. 2017. Loopster: Static Loop Termination Analysis. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering (Paderborn, Germany) (ESEC/FSE 2017). Association for Computing Machinery, New York, NY, USA, 84–94. https://doi.org/10.1145/3106237.3106260

Appendix A Formal Definitions Missing from Main Sections

Definition A.0.

For an annotated program 𝖠\mathsf{A}, the underlying program 𝒞​(𝖠)\mathcal{C}(\mathsf{A}) is the program where the annotations on the while loops have been removed. This is can be formally defined based on the structure of 𝖠\mathsf{A} as follows.

𝒞​(α)\displaystyle\mathcal{C}(\alpha) ≜α\displaystyle\triangleq\alpha
𝒞(if β then 𝖠 else 1𝖠)2\displaystyle\mathcal{C}(\texttt{if }\beta\texttt{ then }\mathsf{A}{{}_{1}}\texttt{ else }\mathsf{A}{{}_{2}}) ≜if β then 𝒞(𝖠)1 else 𝒞(𝖠)2\displaystyle\triangleq\texttt{if }\beta\texttt{ then }\mathcal{C}(\mathsf{A}{{}_{1}})\texttt{ else }\mathcal{C}(\mathsf{A}{{}_{2}})
𝒞(𝖠;1𝖠)2\displaystyle\mathcal{C}(\mathsf{A}{{}_{1}}\>;\>\mathsf{A}{{}_{2}}) ≜𝒞(𝖠)1;𝒞(𝖠)2\displaystyle\triangleq\mathcal{C}(\mathsf{A}{{}_{1}})\>;\>\mathcal{C}(\mathsf{A}{{}_{2}})
𝒞​(𝖨​@​while ​β​ do ​𝖠​ od1)\displaystyle\mathcal{C}(\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}{{}_{1}}\texttt{ od}) ≜while β do 𝒞(𝖠)1 od\displaystyle\triangleq\texttt{while }\beta\texttt{ do }\mathcal{C}(\mathsf{A}{{}_{1}})\texttt{ od}

\inferrule∗[l​a​b=Atomic statements]​α⪯α\inferrule∗[l​a​b=Sequence]​𝖠1′⪯𝖠2′𝖠1′′⪯𝖠2′′​𝖠1′;𝖠1′′⪯𝖠2′;𝖠2′′\inferrule∗[l​a​b=Loop]​𝖨1⊆𝖨2𝖠1′⪯𝖠2′​(𝖨1​@​while​(β)​ do ​𝖠1′​ od )⪯(𝖨2​@​while​(β)​ do ​𝖠2′​ od )\inferrule∗[l​a​b=If]​𝖠1′⪯𝖠2′𝖠1′′⪯𝖠2′′​(if​(β)​ then ​𝖠1′​ else ​𝖠1′′)⪯(if​(β)​ then ​𝖠2′​ else ​𝖠2′′)\begin{array}[]{c}\inferrule*[lab={\footnotesize{\textsc{Atomic statements}}}]{}{\alpha\preceq\alpha}\hskip 28.45274pt\inferrule*[lab={\footnotesize{\textsc{Sequence}}}]{\mathsf{A}^{\prime}_{1}\preceq\mathsf{A}^{\prime}_{2}\quad\mathsf{A}^{\prime\prime}_{1}\preceq\mathsf{A}^{\prime\prime}_{2}}{\mathsf{A}^{\prime}_{1};\mathsf{A}^{\prime\prime}_{1}\preceq\mathsf{A}^{\prime}_{2};\mathsf{A}^{\prime\prime}_{2}}\\ \\ \inferrule*[lab={\footnotesize{\textsc{Loop}}}]{\mathsf{I}_{1}\subseteq\mathsf{I}_{2}\quad\mathsf{A}^{\prime}_{1}\preceq\mathsf{A}^{\prime}_{2}}{\Big{(}\mathsf{I}_{1}\ @\ \texttt{while}(\beta)\texttt{ do }\mathsf{A}^{\prime}_{1}\texttt{ od }\Big{)}\preceq\Big{(}\mathsf{I}_{2}\ @\ \texttt{while}(\beta)\texttt{ do }\mathsf{A}^{\prime}_{2}\texttt{ od }\Big{)}}\\ \\ \inferrule*[lab={\footnotesize{\textsc{If}}}]{\mathsf{A}^{\prime}_{1}\preceq\mathsf{A}^{\prime}_{2}\quad\mathsf{A}^{\prime\prime}_{1}\preceq\mathsf{A}^{\prime\prime}_{2}}{\Big{(}\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{1}\texttt{ else }\mathsf{A}^{\prime\prime}_{1}\Big{)}\preceq\Big{(}\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{2}\texttt{ else }\mathsf{A}^{\prime\prime}_{2}\Big{)}}\end{array}

Figure 8. 𝖠1⪯𝖠2\mathsf{A}_{1}\preceq\mathsf{A}_{2}

\inferrule∗[l​a​b=Atomic statements]​α∧α=α\inferrule∗[l​a​b=Sequence]​𝖠′=𝖠1′∧𝖠2′𝖠′′=𝖠1′′∧𝖠2′′​𝖠1′;𝖠1′′∧𝖠2′;𝖠2′′=𝖠′;𝖠′′\inferrule∗[l​a​b=Loop]​𝖨=𝖨1∩𝖨2𝖠=𝖠1′∧𝖠2′​(𝖨1​@​while​(β)​ do ​𝖠1′​ od )∧(𝖨2​@​while​(β)​ do ​𝖠2′​ od)=𝖨​@​while​(β)​ do ​𝖠​ od \inferrule∗[l​a​b=If]​𝖠′=𝖠1′∧𝖠2′𝖠′′=𝖠1′′∧𝖠2′′​(if​(β)​ then ​𝖠1′​ else ​𝖠1′′)∧(if​(β)​ then ​𝖠2′​ else ​𝖠2′′)=if​(β)​ then ​𝖠′​ else ​𝖠′′\begin{array}[]{c}\inferrule*[lab={\footnotesize{\textsc{Atomic statements}}}]{}{\alpha\wedge\alpha=\alpha}\hskip 28.45274pt\inferrule*[lab={\footnotesize{\textsc{Sequence}}}]{\mathsf{A}^{\prime}=\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\\ \\ \mathsf{A}^{\prime\prime}=\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2}}{\mathsf{A}^{\prime}_{1};\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime}_{2};\mathsf{A}^{\prime\prime}_{2}=\mathsf{A}^{\prime};\mathsf{A}^{\prime\prime}}\\ \\ \inferrule*[lab={\footnotesize{\textsc{Loop}}}]{\mathsf{I}=\mathsf{I}_{1}\cap\mathsf{I}_{2}\quad\mathsf{A}=\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}}{\Big{(}\mathsf{I}_{1}\ @\ \texttt{while}(\beta)\texttt{ do }\mathsf{A}^{\prime}_{1}\texttt{ od }\Big{)}\wedge\Big{(}\mathsf{I}_{2}\ @\ \texttt{while}(\beta)\texttt{ do }\mathsf{A}^{\prime}_{2}\texttt{ od}\Big{)}=\mathsf{I}\ @\ \texttt{while}(\beta)\texttt{ do }\mathsf{A}\texttt{ od }}\\ \\ \inferrule*[lab={\footnotesize{\textsc{If}}}]{\mathsf{A}^{\prime}=\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\quad\mathsf{A}^{\prime\prime}=\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2}}{\Big{(}\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{1}\texttt{ else }\mathsf{A}^{\prime\prime}_{1}\Big{)}\wedge\Big{(}\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{2}\texttt{ else }\mathsf{A}^{\prime\prime}_{2}\Big{)}=\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}\texttt{ else }\mathsf{A}^{\prime\prime}}\end{array}

Figure 9. 𝖠1∧𝖠2\mathsf{A}_{1}\wedge\mathsf{A}_{2}

Appendix B Lemmas and Proofs

Lemma B.0.

If 𝒞(𝖠)1=𝒞(𝖠)2\mathcal{C}(\mathsf{A}{{}_{1}})=\mathcal{C}(\mathsf{A}{{}_{2}}), then ⟦𝖠∧1𝖠⟧2=⟦𝖠⟧1∩⟦𝖠⟧2\llbracket\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\rrbracket=\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket

Proof.

Let 𝒞(𝖠)1=𝒞(𝖠)2=𝖯\mathcal{C}(\mathsf{A}{{}_{1}})=\mathcal{C}(\mathsf{A}{{}_{2}})=\mathsf{P}. We will do the proof by induction on the structure of 𝖯\mathsf{P}.

Case 1 (Base Case): 𝖠≡1𝖠≡2α\mathsf{A}{{}_{1}}\equiv\mathsf{A}{{}_{2}}\equiv\alpha

𝖠∧1𝖠=2α\displaystyle\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}=\alpha …​(1)\displaystyle...(1)
From (1), ⟦𝖠∧1𝖠⟧2=⟦α⟧\displaystyle\text{From (1), }\llbracket\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\rrbracket=\llbracket\alpha\rrbracket …​(2)\displaystyle...(2)
⟦𝖠⟧1=⟦α⟧\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket=\llbracket\alpha\rrbracket …​(3)\displaystyle...(3)
⟦𝖠⟧2=⟦α⟧\displaystyle\llbracket\mathsf{A}{{}_{2}}\rrbracket=\llbracket\alpha\rrbracket …​(4)\displaystyle...(4)
From (3, 4), ⟦𝖠⟧1∩⟦𝖠⟧2=⟦α⟧\displaystyle\text{From (3, 4), }\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket=\llbracket\alpha\rrbracket …​(5)\displaystyle...(5)
From (2, 5), ⟦𝖠∧1𝖠⟧2=⟦𝖠⟧1∩⟦𝖠⟧2\displaystyle\text{From (2, 5), }\llbracket\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\rrbracket=\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket

Case 2: 𝖠≡1𝖨1@while (β) do 𝖠1′ od𝖠≡2𝖨2@while (β) do 𝖠2′ od\mathsf{A}{{}_{1}}\equiv\mathsf{I}_{1}\ @\ \texttt{while }(\beta)\texttt{ do }\mathsf{A}^{\prime}_{1}\texttt{ od}\qquad\mathsf{A}{{}_{2}}\equiv\mathsf{I}_{2}\ @\ \texttt{while }(\beta)\texttt{ do }\mathsf{A}^{\prime}_{2}\texttt{ od}

𝖠∧1𝖠=2(𝖨1∩𝖨2)@while (β) do (𝖠1′∧𝖠2′) od\displaystyle\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}=(\mathsf{I}_{1}\cap\mathsf{I}_{2})\ @\ \texttt{while }(\beta)\texttt{ do }(\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2})\texttt{ od} …​(1)\displaystyle...(1)
From (1), ⟦𝖠∧1𝖠⟧2=(𝖨1∩𝖨2)×(𝖨1∩𝖨2∩⟦¬β⟧)\displaystyle\text{From (1), }\llbracket\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\rrbracket=(\mathsf{I}_{1}\cap\mathsf{I}_{2})\times(\mathsf{I}_{1}\cap\mathsf{I}_{2}\cap\llbracket\neg\beta\rrbracket) …​(2)\displaystyle...(2)
⟦𝖠⟧1=𝖨1×(𝖨1∩⟦¬β⟧)\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket=\mathsf{I}_{1}\times(\mathsf{I}_{1}\cap\llbracket\neg\beta\rrbracket) …​(3)\displaystyle...(3)
⟦𝖠⟧2=𝖨2×(𝖨2∩⟦¬β⟧)\displaystyle\llbracket\mathsf{A}{{}_{2}}\rrbracket=\mathsf{I}_{2}\times(\mathsf{I}_{2}\cap\llbracket\neg\beta\rrbracket) …​(4)\displaystyle...(4)
From (3, 4), ⟦𝖠⟧1∩⟦𝖠⟧2=(𝖨1∩𝖨2)×(𝖨1∩𝖨2∩⟦¬β⟧)\displaystyle\text{From (3, 4), }\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket=(\mathsf{I}_{1}\cap\mathsf{I}_{2})\times(\mathsf{I}_{1}\cap\mathsf{I}_{2}\cap\llbracket\neg\beta\rrbracket) …​(5)\displaystyle...(5)
From (2, 5), ⟦𝖠∧1𝖠⟧2=⟦𝖠⟧1∩⟦𝖠⟧2\displaystyle\text{From (2, 5), }\llbracket\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\rrbracket=\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket

Case 3: 𝖠≡1𝖠1′;𝖠1′′𝖠≡2𝖠2′;𝖠2′′\mathsf{A}{{}_{1}}\equiv\mathsf{A}^{\prime}_{1};\mathsf{A}^{\prime\prime}_{1}\qquad\mathsf{A}{{}_{2}}\equiv\mathsf{A}^{\prime}_{2};\mathsf{A}^{\prime\prime}_{2}

𝖠∧1𝖠=2(𝖠1′∧𝖠2′);(𝖠1′′∧𝖠2′′)\displaystyle\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}=(\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2});(\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2}) …​(1)\displaystyle...(1)
From IH, ⟦𝖠1′∧𝖠2′⟧=⟦(𝖠1′⟧∩⟦𝖠2′)⟧\displaystyle\text{From IH, }\llbracket\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\rrbracket=\llbracket(\mathsf{A}^{\prime}_{1}\rrbracket\cap\llbracket\mathsf{A}^{\prime}_{2})\rrbracket …​(2)\displaystyle...(2)
From IH, ⟦𝖠1′′∧𝖠2′′⟧=⟦(𝖠1′′⟧∩⟦𝖠2′′)⟧\displaystyle\text{From IH, }\llbracket\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2}\rrbracket=\llbracket(\mathsf{A}^{\prime\prime}_{1}\rrbracket\cap\llbracket\mathsf{A}^{\prime\prime}_{2})\rrbracket …​(3)\displaystyle...(3)
⟦(𝖠1′∧𝖠2′);(𝖠1′′∧𝖠2′′)⟧=⟦𝖠1′∧𝖠2′⟧∘⟦𝖠1′∧𝖠2′⟧\displaystyle\llbracket(\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2});(\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2})\rrbracket=\llbracket\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\rrbracket\circ\llbracket\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\rrbracket …​(4)\displaystyle...(4)
⟦𝖠⟧1∩⟦𝖠⟧2=(⟦𝖠1′⟧∘⟦𝖠1′′⟧)∩(⟦𝖠2′⟧∘⟦𝖠2′′⟧)\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket=(\llbracket\mathsf{A}^{\prime}_{1}\rrbracket\circ\llbracket\mathsf{A}^{\prime\prime}_{1}\rrbracket)\cap(\llbracket\mathsf{A}^{\prime}_{2}\rrbracket\circ\llbracket\mathsf{A}^{\prime\prime}_{2}\rrbracket) …​(5)\displaystyle...(5)
From (4, 5), ⟦𝖠∧1𝖠⟧2=⟦𝖠⟧1∩⟦𝖠⟧2\displaystyle\text{From (4, 5), }\llbracket\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\rrbracket=\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket

Case 4: 𝖠≡1if(β) then 𝖠1′ else 𝖠1′′𝖠≡2if(β) then 𝖠2′ else 𝖠2′′\mathsf{A}{{}_{1}}\equiv\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{1}\texttt{ else }\mathsf{A}^{\prime\prime}_{1}\quad\mathsf{A}{{}_{2}}\equiv\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{2}\texttt{ else }\mathsf{A}^{\prime\prime}_{2}

𝖠1∧𝖠2≡if ​(β)​ then ​𝖠1′∧𝖠2′​ else ​𝖠1′′∧𝖠2′′\displaystyle\mathsf{A}_{1}\wedge\mathsf{A}_{2}\equiv\texttt{if }(\beta)\texttt{ then }\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\texttt{ else }\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2} …​(1)\displaystyle...(1)
⟦𝖠∧1𝖠⟧2=𝗂𝖽⟦β⟧∘⟦𝖠1′∧𝖠2′⟧∪𝗂𝖽⟦¬β⟧∘⟦𝖠1′′∧𝖠2′′⟧\displaystyle\llbracket\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\rrbracket=\mathsf{id}_{\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\rrbracket\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2}\rrbracket …​(2)\displaystyle...(2)
From IH, ⟦𝖠1′∧𝖠2′⟧=⟦(𝖠1′⟧∩⟦𝖠2′)⟧\displaystyle\text{From IH, }\llbracket\mathsf{A}^{\prime}_{1}\wedge\mathsf{A}^{\prime}_{2}\rrbracket=\llbracket(\mathsf{A}^{\prime}_{1}\rrbracket\cap\llbracket\mathsf{A}^{\prime}_{2})\rrbracket …​(3)\displaystyle...(3)
From IH, ⟦𝖠1′′∧𝖠2′′⟧=⟦(𝖠1′′⟧∩⟦𝖠2′′)⟧\displaystyle\text{From IH, }\llbracket\mathsf{A}^{\prime\prime}_{1}\wedge\mathsf{A}^{\prime\prime}_{2}\rrbracket=\llbracket(\mathsf{A}^{\prime\prime}_{1}\rrbracket\cap\llbracket\mathsf{A}^{\prime\prime}_{2})\rrbracket …​(4)\displaystyle...(4)
⟦(𝖠∧1𝖠)2⟧=𝗂𝖽⟦β⟧∘(⟦(𝖠1′⟧∩⟦𝖠2′)⟧)∪𝗂𝖽⟦¬β⟧∘(⟦(𝖠1′′⟧∩⟦𝖠2′′)⟧)\displaystyle\llbracket(\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}})\rrbracket=\mathsf{id}_{\llbracket\beta\rrbracket}\circ(\llbracket(\mathsf{A}^{\prime}_{1}\rrbracket\cap\llbracket\mathsf{A}^{\prime}_{2})\rrbracket)\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ(\llbracket(\mathsf{A}^{\prime\prime}_{1}\rrbracket\cap\llbracket\mathsf{A}^{\prime\prime}_{2})\rrbracket) …​(5)\displaystyle...(5)
⟦𝖠⟧1=𝗂𝖽⟦β⟧∘⟦(𝖠1′⟧∪𝗂𝖽⟦¬β⟧∘⟦𝖠1′′⟧\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket=\mathsf{id}_{\llbracket\beta\rrbracket}\circ\llbracket(\mathsf{A}^{\prime}_{1}\rrbracket\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime\prime}_{1}\rrbracket …​(6)\displaystyle...(6)
⟦𝖠⟧2=𝗂𝖽⟦β⟧∘⟦(𝖠2′⟧∪𝗂𝖽⟦¬β⟧∘⟦𝖠2′′⟧\displaystyle\llbracket\mathsf{A}{{}_{2}}\rrbracket=\mathsf{id}_{\llbracket\beta\rrbracket}\circ\llbracket(\mathsf{A}^{\prime}_{2}\rrbracket\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime\prime}_{2}\rrbracket …​(7)\displaystyle...(7)
From (5, 6, 7), ⟦𝖠1∧𝖠2⟧=⟦𝖠⟧1∩⟦𝖠⟧2\displaystyle\text{From (5, 6, 7), }\llbracket\mathsf{A}_{1}\wedge\mathsf{A}_{2}\rrbracket=\llbracket\mathsf{A}{{}_{1}}\rrbracket\cap\llbracket\mathsf{A}{{}_{2}}\rrbracket

∎

Lemma B.0.

If

  1. (1)

    S⊧𝖠S\models\mathsf{A}

  2. (2)

    S′⊆SS^{\prime}\subseteq S

Then S′⊧𝖠S^{\prime}\models\mathsf{A}

Proof.

We do this by induction on the structure of the underlying program 𝒞​(𝖠)\mathcal{C}(\mathsf{A}):
Base Case: 𝖠=α\mathsf{A}=\alpha
The proof holds trivially from the rules of atomic statements as S′⊧αS^{\prime}\models\alpha holds for all S′S^{\prime}.

Inductive Case:
Case 1: 𝖠≡if​(β)​ then ​𝖠1​ else ​𝖠2\mathsf{A}\equiv\texttt{if}(\beta)\texttt{ then }\mathsf{A}_{1}\texttt{ else }\mathsf{A}_{2}

S⊧𝖠\displaystyle S\models\mathsf{A} Antecedant (1) …​(1)\displaystyle...(1)
From (1), S∩⟦β⟧⊧𝖠1\displaystyle\text{From (1), }S\cap\llbracket\beta\rrbracket\models\mathsf{A}{{}_{1}} …​(2)\displaystyle...(2)
S∩⟦¬β⟧⊧𝖠2\displaystyle S\cap\llbracket\neg\beta\rrbracket\models\mathsf{A}{{}_{2}} …​(3)\displaystyle...(3)
S′⊆S\displaystyle S^{\prime}\subseteq S Antecedant (2) …​(4)\displaystyle...(4)
From (2, 4), using IH, S′∩⟦β⟧⊧𝖠1\displaystyle\text{From (2, 4), using IH, }S^{\prime}\cap\llbracket\beta\rrbracket\models\mathsf{A}{{}_{1}} …​(5)\displaystyle...(5)
From (3, 4), using IH, S′∩⟦¬β⟧⊧𝖠2\displaystyle\text{From (3, 4), using IH, }S^{\prime}\cap\llbracket\neg\beta\rrbracket\models\mathsf{A}{{}_{2}} …​(6)\displaystyle...(6)
From (5, 6), using IH, ​S′⊧if​(β)​ then ​𝖠1​ else ​𝖠2\displaystyle\text{From (5, 6), using IH, }S^{\prime}\models\texttt{if}(\beta)\texttt{ then }\mathsf{A}_{1}\texttt{ else }\mathsf{A}_{2} Consequent

Case 2: 𝖠≡𝖠1;𝖠2\mathsf{A}\equiv\mathsf{A}_{1}\;;\;\mathsf{A}_{2}

S⊧𝖠\displaystyle S\models\mathsf{A} Antecedant (1) …​(1)\displaystyle...(1)
From (1), S⊧𝖠1\displaystyle\text{From (1), }S\models\mathsf{A}{{}_{1}} …​(2)\displaystyle...(2)
S∘⟦𝖠⟧1⊧𝖠2\displaystyle S\circ\llbracket\mathsf{A}{{}_{1}}\rrbracket\models\mathsf{A}{{}_{2}} …​(3)\displaystyle...(3)
S′⊆S\displaystyle S^{\prime}\subseteq S Antecedant (2) …​(4)\displaystyle...(4)
From (2, 4), using IH, S′⊧𝖠1\displaystyle\text{From (2, 4), using IH, }S^{\prime}\models\mathsf{A}{{}_{1}} …​(5)\displaystyle...(5)
From (3, 4), using IH, S′∘⟦𝖠⟧1⊧𝖠2\displaystyle\text{From (3, 4), using IH, }S^{\prime}\circ\llbracket\mathsf{A}{{}_{1}}\rrbracket\models\mathsf{A}{{}_{2}} …​(6)\displaystyle...(6)
From (5, 6), using IH, S′⊧𝖠;1𝖠2\displaystyle\text{From (5, 6), using IH, }S^{\prime}\models\mathsf{A}{{}_{1}};\mathsf{A}{{}_{2}} Consequent

Case 3: 𝖠≡𝖨​@​while​(β)​ do ​𝖠​ od1\mathsf{A}\equiv\mathsf{I}\;@\;\texttt{while}(\beta)\texttt{ do }\mathsf{A}{{}_{1}}\texttt{ od}

S⊧𝖠\displaystyle S\models\mathsf{A} Antecedant (1) …​(1)\displaystyle...(1)
From (1), ​S⊆𝖨\displaystyle\text{From (1), }S\subseteq\mathsf{I} …​(2)\displaystyle...(2)
𝖨∩⟦β⟧∘⟦𝖠⟧1⊆𝖨\displaystyle\mathsf{I}\cap\llbracket\beta\rrbracket\circ\llbracket\mathsf{A}{{}_{1}}\rrbracket\subseteq\mathsf{I} …​(3)\displaystyle...(3)
𝖨∩⟦β⟧⊧𝖠1\displaystyle\mathsf{I}\cap\llbracket\beta\rrbracket\models\mathsf{A}{{}_{1}} …​(4)\displaystyle...(4)
S′⊆S\displaystyle S^{\prime}\subseteq S Antecedant (2) …​(5)\displaystyle...(5)
From (2, 5), using IH, ​S⊧𝖨\displaystyle\text{From (2, 5), using IH, }S\models\mathsf{I} …​(6)\displaystyle...(6)
From (3, 4, 6), using IH, ​S′⊧𝖨​@​while​(β)​ do ​𝖠​ od1\displaystyle\text{From (3, 4, 6), using IH, }S^{\prime}\models\mathsf{I}\;@\;\texttt{while}(\beta)\texttt{ do }\mathsf{A}{{}_{1}}\texttt{ od} Consequent

∎

Lemma B.0.

If

  1. (1)

    S⊧𝖠1S\models\mathsf{A}{{}_{1}}

  2. (2)

    S⊧𝖠2S\models\mathsf{A}{{}_{2}}

  3. (3)

    𝒞(𝖠)1=𝒞(𝖠)2\mathcal{C}(\mathsf{A}{{}_{1}})=\mathcal{C}(\mathsf{A}{{}_{2}})

Then S⊧𝖠∧1𝖠2S\models\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}

Proof.

𝒞(𝖠)1=𝒞(𝖠)2\mathcal{C}(\mathsf{A}{{}_{1}})=\mathcal{C}(\mathsf{A}{{}_{2}}) ensures that the meet 𝖠∧1𝖠2\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}} is defined as we define it only for annotated programs with the same underlying program. Let 𝒞(𝖠)1=𝒞(𝖠)2=𝖯\mathcal{C}(\mathsf{A}{{}_{1}})=\mathcal{C}(\mathsf{A}{{}_{2}})=\mathsf{P}. We will do the proof by induction on the structure of 𝖯\mathsf{P}.
Base Case: 𝖠=1𝖠=2α\mathsf{A}{{}_{1}}=\mathsf{A}{{}_{2}}=\alpha
In this case, 𝖠3=𝖠∧1𝖠=2α\mathsf{A}_{3}=\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}=\alpha. As we are given S⊧𝖠(=α)1S\models\mathsf{A}{{}_{1}}(=\alpha), it follows that S⊧𝖠3(=α)S\models\mathsf{A}_{3}(=\alpha).

Inductive Case:
Case 1: 𝖠=1if(β) then 𝖠11 else 𝖠12𝖠=2if(β) then 𝖠21 else 𝖠22\mathsf{A}{{}_{1}}=\texttt{if}(\beta)\texttt{ then }\mathsf{A}_{11}\texttt{ else }\mathsf{A}_{12}\quad\mathsf{A}{{}_{2}}=\texttt{if}(\beta)\texttt{ then }\mathsf{A}_{21}\texttt{ else }\mathsf{A}_{22}

S⊧𝖠1\displaystyle S\models\mathsf{A}{{}_{1}} Antecedant (1) …​(1)\displaystyle...(1)
From (1), (S∩⟦β⟧)⊧𝖠11\displaystyle\text{From (1), }(S\cap\llbracket\beta\rrbracket)\models\mathsf{A}_{11} …​(2)\displaystyle...(2)
(S∩⟦¬β⟧)⊧𝖠12\displaystyle(S\cap\llbracket\neg\beta\rrbracket)\models\mathsf{A}_{12} …​(3)\displaystyle...(3)
S⊧𝖠2\displaystyle S\models\mathsf{A}{{}_{2}} Antecedant (2) …​(4)\displaystyle...(4)
From (4), (S∩⟦β⟧)⊧𝖠21\displaystyle\text{From (4), }(S\cap\llbracket\beta\rrbracket)\models\mathsf{A}_{21} …​(5)\displaystyle...(5)
(S∩⟦¬β⟧)⊧𝖠22\displaystyle(S\cap\llbracket\neg\beta\rrbracket)\models\mathsf{A}_{22} …​(6)\displaystyle...(6)
From (2, 5), using IH, (S∩⟦β⟧)⊧𝖠11∧𝖠21\displaystyle\text{From (2, 5), using IH, }(S\cap\llbracket\beta\rrbracket)\models\mathsf{A}_{11}\wedge\mathsf{A}_{21} …​(7)\displaystyle...(7)
From (3, 6), using IH, (S∩⟦¬β⟧)⊧𝖠12∧𝖠22\displaystyle\text{From (3, 6), using IH, }(S\cap\llbracket\neg\beta\rrbracket)\models\mathsf{A}_{12}\wedge\mathsf{A}_{22} …​(8)\displaystyle...(8)
From (7,8), S⊧𝖠∧1𝖠2\displaystyle\text{From (7,8), }S\models\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}} Consequent

Case 2: 𝖠=1𝖠11;𝖠12𝖠=2𝖠21;𝖠22\mathsf{A}{{}_{1}}=\mathsf{A}_{11}\;;\;\mathsf{A}_{12}\quad\mathsf{A}{{}_{2}}=\mathsf{A}_{21}\;;\;\mathsf{A}_{22}

S⊧𝖠1\displaystyle S\models\mathsf{A}{{}_{1}} Antecedant (1) …​(1)\displaystyle...(1)
From (1), ​S⊧𝖠11\displaystyle\text{From (1), }S\models\mathsf{A}_{11} …​(2)\displaystyle...(2)
(S∘⟦𝖠11⟧)⊧𝖠12\displaystyle(S\circ\llbracket\mathsf{A}_{11}\rrbracket)\models\mathsf{A}_{12} …​(3)\displaystyle...(3)
S⊧𝖠2\displaystyle S\models\mathsf{A}{{}_{2}} Antecedant (2) …​(4)\displaystyle...(4)
From (4), ​S⊧𝖠21\displaystyle\text{From (4), }S\models\mathsf{A}_{21} …​(5)\displaystyle...(5)
(S∘⟦𝖠21⟧)⊧𝖠22\displaystyle(S\circ\llbracket\mathsf{A}_{21}\rrbracket)\models\mathsf{A}_{22} …​(6)\displaystyle...(6)
From (2, 5), using IH, ​S⊧𝖠11∧𝖠21\displaystyle\text{From (2, 5), using IH, }S\models\mathsf{A}_{11}\wedge\mathsf{A}_{21} …​(7)\displaystyle...(7)
From lemma B.1, S∘⟦(𝖠11∧𝖠21)⟧)≡S∘(⟦𝖠11⟧∩⟦𝖠21⟧)\displaystyle\text{From lemma~{}\ref{aplemma:annos}, }S\circ\llbracket(\mathsf{A}_{11}\wedge\mathsf{A}_{21})\rrbracket)\equiv S\circ(\llbracket\mathsf{A}_{11}\rrbracket\cap\llbracket\mathsf{A}_{21}\rrbracket) …​(8)\displaystyle...(8)
From (8), S∘⟦(𝖠11∧𝖠21)⟧)⊆(S∘⟦𝖠11⟧)\displaystyle\text{From (8), }S\circ\llbracket(\mathsf{A}_{11}\wedge\mathsf{A}_{21})\rrbracket)\subseteq(S\circ\llbracket\mathsf{A}_{11}\rrbracket) …​(9)\displaystyle...(9)
From (8), S∘⟦(𝖠11∧𝖠21)⟧)⊆(S∘⟦𝖠21⟧)\displaystyle\text{From (8), }S\circ\llbracket(\mathsf{A}_{11}\wedge\mathsf{A}_{21})\rrbracket)\subseteq(S\circ\llbracket\mathsf{A}_{21}\rrbracket) …​(10)\displaystyle...(10)
From (9), using Lemma B.2, S∘⟦(𝖠11∧𝖠21)⟧)⊧𝖠12\displaystyle\text{From (9), using Lemma~{}\ref{aplemma:less}, }S\circ\llbracket(\mathsf{A}_{11}\wedge\mathsf{A}_{21})\rrbracket)\models\mathsf{A}_{12} …​(11)\displaystyle...(11)
From (10), using Lemma B.2, S∘⟦(𝖠11∧𝖠21)⟧)⊧𝖠22\displaystyle\text{From (10), using Lemma~{}\ref{aplemma:less}, }S\circ\llbracket(\mathsf{A}_{11}\wedge\mathsf{A}_{21})\rrbracket)\models\mathsf{A}_{22} …​(12)\displaystyle...(12)
From (11, 12), using IH, S∘⟦(𝖠11∧𝖠21)⟧)⊧𝖠12∧𝖠22\displaystyle\text{From (11, 12), using IH, }S\circ\llbracket(\mathsf{A}_{11}\wedge\mathsf{A}_{21})\rrbracket)\models\mathsf{A}_{12}\wedge\mathsf{A}_{22} …​(13)\displaystyle...(13)
From (7, 13), S⊧𝖠∧1𝖠2\displaystyle\text{From (7, 13), }S\models\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}} Consequent

Case 3: 𝖠≡1𝖨1@while(β) do 𝖠11 od𝖠≡2𝖨2@while(β) do 𝖠21 od\mathsf{A}{{}_{1}}\equiv\mathsf{I}_{1}\;@\;\texttt{while}(\beta)\texttt{ do }\mathsf{A}_{11}\texttt{ od}\quad\mathsf{A}{{}_{2}}\equiv\mathsf{I}_{2}\;@\;\texttt{while}(\beta)\texttt{ do }\mathsf{A}_{21}\texttt{ od}

S⊧𝖠1\displaystyle S\models\mathsf{A}{{}_{1}} Antecedant (1) …​(1)\displaystyle...(1)
From (1), ​S⊆𝖨1\displaystyle\text{From (1), }S\subseteq\mathsf{I}_{1} …​(2)\displaystyle...(2)
𝖨1∩⟦β⟧∘⟦𝖠11⟧⊆𝖨1\displaystyle\mathsf{I}_{1}\cap\llbracket\beta\rrbracket\circ\llbracket\mathsf{A}_{11}\rrbracket\subseteq\mathsf{I}_{1} …​(3)\displaystyle...(3)
𝖨1∩⟦β⟧⊧𝖠11\displaystyle\mathsf{I}_{1}\cap\llbracket\beta\rrbracket\models\mathsf{A}_{11} …​(4)\displaystyle...(4)
S⊧𝖠2\displaystyle S\models\mathsf{A}{{}_{2}} Antecedant (2) …​(5)\displaystyle...(5)
From (5), ​S⊆𝖨2\displaystyle\text{From (5), }S\subseteq\mathsf{I}_{2} …​(6)\displaystyle...(6)
𝖨2∩⟦β⟧∘⟦𝖠21⟧⊆𝖨2\displaystyle\mathsf{I}_{2}\cap\llbracket\beta\rrbracket\circ\llbracket\mathsf{A}_{21}\rrbracket\subseteq\mathsf{I}_{2} …​(7)\displaystyle...(7)
𝖨2∩⟦β⟧⊧𝖠21\displaystyle\mathsf{I}_{2}\cap\llbracket\beta\rrbracket\models\mathsf{A}_{21} …​(8)\displaystyle...(8)
From (2, 6), ​S⊆𝖨1∩𝖨2\displaystyle\text{From (2, 6), }S\subseteq\mathsf{I}_{1}\cap\mathsf{I}_{2} …​(9)\displaystyle...(9)
From (3, 7), (𝖨1∩𝖨2∩⟦β⟧)∘⟦𝖠11∧𝖠21⟧⊆(𝖨1∩𝖨2)\displaystyle\text{From (3, 7), }(\mathsf{I}_{1}\cap\mathsf{I}_{2}\cap\llbracket\beta\rrbracket)\circ\llbracket\mathsf{A}_{11}\wedge\mathsf{A}_{21}\rrbracket\subseteq(\mathsf{I}_{1}\cap\mathsf{I}_{2}) …​(10)\displaystyle...(10)
From 4 using Lemma B.2, 𝖨1∩𝖨2∩⟦β⟧⊧𝖠11\displaystyle\text{From 4 using Lemma~{}\ref{aplemma:less}, }\mathsf{I}_{1}\cap\mathsf{I}_{2}\cap\llbracket\beta\rrbracket\models\mathsf{A}_{11} …​(11)\displaystyle...(11)
From 8 using Lemma B.2, 𝖨1∩𝖨2∩⟦β⟧⊧𝖠21\displaystyle\text{From 8 using Lemma~{}\ref{aplemma:less}, }\mathsf{I}_{1}\cap\mathsf{I}_{2}\cap\llbracket\beta\rrbracket\models\mathsf{A}_{21} …​(12)\displaystyle...(12)
From (10, 11, 12), using IH, S⊧𝖠∧1𝖠2\displaystyle\text{From (10, 11, 12), using IH, }S\models\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}} Consequent

∎

Lemma B.0.

If 𝖠,1𝖠∈2ℒ(L,ℐ)\mathsf{A}{{}_{1}},\mathsf{A}{{}_{2}}\in\mathcal{L}(L,\mathcal{I}) satisfy:

  1. (1)

    Init⊧𝖠1Init\models\mathsf{A}{{}_{1}}

  2. (2)

    Init⊧𝖠2Init\models\mathsf{A}{{}_{2}}

  3. (3)

    ℐ\mathcal{I} is closed under intersection

then 𝖠∧1𝖠∈2ℒ(L,ℐ)\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}\in\mathcal{L}(L,\mathcal{I}) and Init⊧𝖠∧1𝖠2Init\models\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}}.

Proof.

ℐ\mathcal{I} being closed under intersection takes care of the fact that 𝖠3=𝖠∧1𝖠2\mathsf{A}_{3}=\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}} is in ℒ​(L,ℐ)\mathcal{L}(L,\mathcal{I}) as the meet operator takes the intersection of invariants in 𝖠1\mathsf{A}{{}_{1}} and 𝖠2\mathsf{A}{{}_{2}}. Now, as Init⊧𝖠1Init\models\mathsf{A}{{}_{1}} and Init⊧𝖠2Init\models\mathsf{A}{{}_{2}}, Init⊧𝖠∧1𝖠2Init\models\mathsf{A}{{}_{1}}\wedge\mathsf{A}{{}_{2}} follows directly from the lemma B.3. ∎

Lemma B.0.

If 𝒞(𝖠)1=𝒞(𝖠)2\mathcal{C}(\mathsf{A}{{}_{1}})=\mathcal{C}(\mathsf{A}{{}_{2}}), then 𝖠⪯1𝖠⟹2⟦𝖠⟧1⊆⟦𝖠⟧2\mathsf{A}{{}_{1}}\preceq\mathsf{A}{{}_{2}}\implies\llbracket\mathsf{A}{{}_{1}}\rrbracket\subseteq\llbracket\mathsf{A}{{}_{2}}\rrbracket

Proof.

Let 𝒞(𝖠)1=𝒞(𝖠)2=𝖯\mathcal{C}(\mathsf{A}{{}_{1}})=\mathcal{C}(\mathsf{A}{{}_{2}})=\mathsf{P}. We will do the proof by induction on the structure of 𝖯\mathsf{P}.

Case 1 (Base case): 𝖠≡1𝖠≡2α\mathsf{A}{{}_{1}}\equiv\mathsf{A}{{}_{2}}\equiv\alpha

⟦𝖠⟧1=α\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket=\alpha …​(1)\displaystyle...(1)
⟦𝖠⟧2=α\displaystyle\llbracket\mathsf{A}{{}_{2}}\rrbracket=\alpha …​(2)\displaystyle...(2)
From (1, 2), ⟦𝖠⟧1⊆⟦𝖠⟧2\displaystyle\text{From (1, 2), }\llbracket\mathsf{A}{{}_{1}}\rrbracket\subseteq\llbracket\mathsf{A}{{}_{2}}\rrbracket …​(3)\displaystyle...(3)

Case 2: 𝖠≡1𝖨1@while (β) do 𝖠1′ od𝖠≡2𝖨2@while (β) do 𝖠2′ od\mathsf{A}{{}_{1}}\equiv\mathsf{I}_{1}\ @\ \texttt{while }(\beta)\texttt{ do }\mathsf{A}^{\prime}_{1}\texttt{ od}\qquad\mathsf{A}{{}_{2}}\equiv\mathsf{I}_{2}\ @\ \texttt{while }(\beta)\texttt{ do }\mathsf{A}^{\prime}_{2}\texttt{ od}

From (𝖠⪯1𝖠)2,𝖨1⊆𝖨2\displaystyle\text{From }(\mathsf{A}{{}_{1}}\preceq\mathsf{A}{{}_{2}}),\;\mathsf{I}_{1}\subseteq\mathsf{I}_{2} …​(1)\displaystyle...(1)
⟦𝖠⟧1=𝖨1×(𝖨1∩⟦¬β⟧)\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket=\mathsf{I}_{1}\times(\mathsf{I}_{1}\cap\llbracket\neg\beta\rrbracket) …​(2)\displaystyle...(2)
⟦𝖠⟧2=𝖨2×(𝖨2∩⟦¬β⟧)\displaystyle\llbracket\mathsf{A}{{}_{2}}\rrbracket=\mathsf{I}_{2}\times(\mathsf{I}_{2}\cap\llbracket\neg\beta\rrbracket) …​(3)\displaystyle...(3)
From (1, 2, 3), ⟦𝖠⟧1⊆⟦𝖠⟧2\displaystyle\text{From (1, 2, 3), }\llbracket\mathsf{A}{{}_{1}}\rrbracket\subseteq\llbracket\mathsf{A}{{}_{2}}\rrbracket …​(4)\displaystyle...(4)

Case 3: 𝖠≡1𝖠1′;𝖠1′′𝖠≡2𝖠2′;𝖠2′′\mathsf{A}{{}_{1}}\equiv\mathsf{A}^{\prime}_{1};\mathsf{A}^{\prime\prime}_{1}\qquad\mathsf{A}{{}_{2}}\equiv\mathsf{A}^{\prime}_{2};\mathsf{A}^{\prime\prime}_{2}

From (𝖠⪯1𝖠)2,𝖠1′⪯𝖠2′∧𝖠1′′⪯𝖠2′′\displaystyle\text{From }(\mathsf{A}{{}_{1}}\preceq\mathsf{A}{{}_{2}}),\;\mathsf{A}^{\prime}_{1}\preceq\mathsf{A}^{\prime}_{2}\wedge\mathsf{A}^{\prime\prime}_{1}\preceq\mathsf{A}^{\prime\prime}_{2} …​(1)\displaystyle...(1)
⟦𝖠⟧1=⟦𝖠1′⟧∘⟦𝖠1′′⟧\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket=\llbracket\mathsf{A}^{\prime}_{1}\rrbracket\circ\llbracket\mathsf{A}^{\prime\prime}_{1}\rrbracket …​(2)\displaystyle...(2)
⟦𝖠⟧2=⟦𝖠2′⟧∘⟦𝖠2′′⟧\displaystyle\llbracket\mathsf{A}{{}_{2}}\rrbracket=\llbracket\mathsf{A}^{\prime}_{2}\rrbracket\circ\llbracket\mathsf{A}^{\prime\prime}_{2}\rrbracket …​(3)\displaystyle...(3)
From 1 using IH, ⟦𝖠1′⟧⊆⟦𝖠2′⟧\displaystyle\text{From 1 using IH, }\llbracket\mathsf{A}^{\prime}_{1}\rrbracket\subseteq\llbracket\mathsf{A}^{\prime}_{2}\rrbracket …​(4)\displaystyle...(4)
From 1 using IH, ⟦𝖠1′′⟧⊆⟦𝖠2′′⟧\displaystyle\text{From 1 using IH, }\llbracket\mathsf{A}^{\prime\prime}_{1}\rrbracket\subseteq\llbracket\mathsf{A}^{\prime\prime}_{2}\rrbracket …​(5)\displaystyle...(5)
From (2,3,4,5), ⟦𝖠⟧1⊆⟦𝖠⟧2\displaystyle\text{From (2,3,4,5), }\llbracket\mathsf{A}{{}_{1}}\rrbracket\subseteq\llbracket\mathsf{A}{{}_{2}}\rrbracket …​(6)\displaystyle...(6)

Case 4: 𝖠≡1if(β) then 𝖠1′ else 𝖠1′′𝖠≡2if(β) then 𝖠2′ else 𝖠2′′\mathsf{A}{{}_{1}}\equiv\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{1}\texttt{ else }\mathsf{A}^{\prime\prime}_{1}\qquad\mathsf{A}{{}_{2}}\equiv\texttt{if}(\beta)\texttt{ then }\mathsf{A}^{\prime}_{2}\texttt{ else }\mathsf{A}^{\prime\prime}_{2}

From (𝖠⪯1𝖠)2,𝖠1′⪯𝖠2′∧𝖠1′′⪯𝖠2′′\displaystyle\text{From }(\mathsf{A}{{}_{1}}\preceq\mathsf{A}{{}_{2}}),\;\mathsf{A}^{\prime}_{1}\preceq\mathsf{A}^{\prime}_{2}\wedge\mathsf{A}^{\prime\prime}_{1}\preceq\mathsf{A}^{\prime\prime}_{2} …​(1)\displaystyle...(1)
⟦𝖠⟧1=𝗂𝖽⟦β⟧∘⟦𝖠1′⟧∪𝗂𝖽⟦¬β⟧∘⟦𝖠1′′⟧\displaystyle\llbracket\mathsf{A}{{}_{1}}\rrbracket=\mathsf{id}_{\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}_{1}\rrbracket\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime\prime}_{1}\rrbracket …​(2)\displaystyle...(2)
⟦𝖠⟧2=𝗂𝖽⟦β⟧∘⟦𝖠2′⟧∪𝗂𝖽⟦¬β⟧∘⟦𝖠2′′⟧\displaystyle\llbracket\mathsf{A}{{}_{2}}\rrbracket=\mathsf{id}_{\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}_{2}\rrbracket\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime\prime}_{2}\rrbracket …​(3)\displaystyle...(3)
From 1 using IH, ⟦𝖠1′⟧⊆⟦𝖠2′⟧\displaystyle\text{From 1 using IH, }\llbracket\mathsf{A}^{\prime}_{1}\rrbracket\subseteq\llbracket\mathsf{A}^{\prime}_{2}\rrbracket …​(4)\displaystyle...(4)
From 1 using IH, ⟦𝖠1′′⟧⊆⟦𝖠2′′⟧\displaystyle\text{From 1 using IH, }\llbracket\mathsf{A}^{\prime\prime}_{1}\rrbracket\subseteq\llbracket\mathsf{A}^{\prime\prime}_{2}\rrbracket …​(5)\displaystyle...(5)
From (2,3,4,5), ⟦𝖠⟧1⊆⟦𝖠⟧2\displaystyle\text{From (2,3,4,5), }\llbracket\mathsf{A}{{}_{1}}\rrbracket\subseteq\llbracket\mathsf{A}{{}_{2}}\rrbracket …​(6)\displaystyle...(6)

∎

Lemma B.0.

If

  1. (1)

    Init⊧𝖠𝖫,1fInit\models\mathsf{A}_{\mathsf{L}}{{}_{1}},f

  2. (2)

    Init⊧𝖠𝖫2Init\models\mathsf{A}_{\mathsf{L}}{{}_{2}}

  3. (3)

    𝖠𝖫⪯2𝖠𝖫1\mathsf{A}_{\mathsf{L}}{{}_{2}}\preceq\mathsf{A}_{\mathsf{L}}{{}_{1}}

then Init⊧𝖠𝖫,2fInit\models\mathsf{A}_{\mathsf{L}}{{}_{2}},f

Proof.

Recall from Section 3, that 𝖠𝖫\mathsf{A}_{\mathsf{L}} is an annotated loop program 𝖠𝖫=𝖨​@​while ​β​ do ​𝖠​ od\mathsf{A}_{\mathsf{L}}=\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}\texttt{ od}. From definition 4.1 As defined in Section 3, Init⊧𝖠𝖫,2fInit\models\mathsf{A}_{\mathsf{L}}{{}_{2}},f holds when Init⊧𝖠𝖫2Init\models\mathsf{A}_{\mathsf{L}}{{}_{2}} (already given) and ff is valid for the loop program 𝖠𝖫=2𝖨2@while(β) do 𝖠2′ od\mathsf{A}_{\mathsf{L}}{{}_{2}}=\mathsf{I}_{2}\;@\;\texttt{while}(\beta)\texttt{ do }\mathsf{A}^{\prime}_{2}\texttt{ od}. We are given that ff is valid for loop program 𝖠𝖫=1𝖨1@while(β) do 𝖠1′ od\mathsf{A}_{\mathsf{L}}{{}_{1}}=\mathsf{I}_{1}\;@\;\texttt{while}(\beta)\texttt{ do }\mathsf{A}^{\prime}_{1}\texttt{ od}, i.e. it satisfies

∀(s,s′)∈𝗂𝖽𝖨1∩⁣⟦β⟧∘⟦𝖠⟧1,f(s)≥0 and f(s)−f(s′)≥1\forall(s,s^{\prime})\in\mathsf{id}_{\mathsf{I}_{1}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}{{}_{1}}\rrbracket,f(s)\geq 0\text{ and }f(s)-f(s^{\prime})\geq 1

.

Also, 𝖠⪯2𝖠⟹1(𝖨2⊆𝖨1)∧(𝖠2′⪯𝖠1′)\mathsf{A}{{}_{2}}\preceq\mathsf{A}{{}_{1}}\implies(\mathsf{I}_{2}\subseteq\mathsf{I}_{1})\wedge(\mathsf{A}^{\prime}_{2}\preceq\mathsf{A}^{\prime}_{1}), which is equivalent to (𝖨2⊆𝖨1)∧(⟦𝖠2′⟧⊆⟦𝖠1′⟧)(\mathsf{I}_{2}\subseteq\mathsf{I}_{1})\wedge(\llbracket\mathsf{A}^{\prime}_{2}\rrbracket\subseteq\llbracket\mathsf{A}^{\prime}_{1}\rrbracket) from lemma B.5. This implies that (𝗂𝖽𝖨2∩⁣⟦β⟧∘⟦𝖠⟧2)⊆(𝗂𝖽𝖨1∩⁣⟦β⟧∘⟦𝖠⟧1)(\mathsf{id}_{\mathsf{I}_{2}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}{{}_{2}}\rrbracket)\subseteq(\mathsf{id}_{\mathsf{I}_{1}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}{{}_{1}}\rrbracket). So, from the definition of ff being valid for 𝖠𝖫1\mathsf{A}_{\mathsf{L}}{{}_{1}}, we can also say:

∀(s,s′)∈𝗂𝖽𝖨2∩⁣⟦β⟧∘⟦𝖠⟧2,f(s)≥0 and f(s)−f(s′)≥1\forall(s,s^{\prime})\in\mathsf{id}_{\mathsf{I}_{2}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}{{}_{2}}\rrbracket,f(s)\geq 0\text{ and }f(s)-f(s^{\prime})\geq 1

.

This proves that Init⊧𝖠𝖫,2fInit\models\mathsf{A}_{\mathsf{L}}{{}_{2}},f. ∎

Proof for Proposition 4.2:

  1. (1)

    I​n​i​t⊧𝖠2Init\models\mathsf{A}_{2} and I​n​i​t⊧𝖠1Init\models\mathsf{A}_{1}, then I​n​i​t⊧𝖠1∧𝖠2Init\models\mathsf{A}_{1}\wedge\mathsf{A}_{2} follows from lemma  B.4.

  2. (2)

    If I​n​i​t⊧𝖠1,fInit\models\mathsf{A}_{1},f, I​n​i​t⊧𝖠2Init\models\mathsf{A}_{2}, and 𝖠2⪯𝖠1\mathsf{A}_{2}\preceq\mathsf{A}_{1}, then I​n​i​t⊧𝖠2,fInit\models\mathsf{A}_{2},f follows from Lemma B.6

Appendix C Ablation Studies

Refer to caption
(a) Template ℱ1\mathcal{F}_{1}
Refer to caption
(b) Template ℱ2\mathcal{F}_{2}
Refer to caption
(c) Template ℱ3\mathcal{F}_{3}
Refer to caption
(d) Template ℱ4\mathcal{F}_{4}
Refer to caption
(e) Template ℱ5\mathcal{F}_{5}
Figure 10. Percentage of benchmarks proved terminating with growing running time.