Non-polynomial Worst-Case Analysis of Recursive Programs

TL;DR

This paper introduces a novel approach for proving non-polynomial worst-case bounds of recursive programs using measure functions synthesized through linear programming, enabling bounds like n log n and non-integer polynomial exponents.

Contribution

The paper extends ranking functions to recursion, enabling synthesis of non-polynomial measure functions with logarithmic and exponential forms using linear programming techniques.

Findings

Successfully synthesized bounds for classical recursive algorithms

Achieved bounds such as O(n log n) for Merge-Sort

Obtained non-integer polynomial bounds close to best-known results

Abstract

We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of nonrecursive programs. First, we apply ranking functions to recursion, resulting in measure functions. We show that measure functions provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in nonpolynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form $\mathcal{O}(n\log n)$ as well as $\mathcal{O}(n^r)$ where $r$ is not an integer. We present experimental results to demonstrate that our approach can obtain efficiently worst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the divide-and-conquer algorithm for the Closest-Pair problem, where we obtain $\mathcal{O}(n \log n)$ worst-case bound, and (ii) Karatsuba's algorithm for polynomial multiplication and Strassen's algorithm for matrix multiplication, where we obtain $\mathcal{O}(n^r)$ bound such that $r$ is not an integer and close to the best-known bounds for the respective algorithms.

Tables

Table 1. Table 1: Experimental results where η ​ ( ℓ 0 ) 𝜂 subscript ℓ 0 \eta(\ell_{0}) is the part of measure function at the initial label.

Example	Time (in Seconds)	$\eta \left({\ell }_0\right)$
Merge-Sort	6	$25.02\cdot n\cdot \ln n+21.68\cdot n-20.68$
Closest-Pair	11	$128.85\cdot n\cdot \ln n+108.95\cdot n-53.31$
Karatsuba	3	$2261.55\cdot n^{1.6}+1$
Strassen	7	$954.2\cdot n^{2.9}+1$

Table 2. Table 2: Invariants Used for Significant Labels

$𝖿$	$\ell$	$I(𝖿,\ell )$
$\mathrm{𝗆𝖾𝗋𝗀𝖾𝗌𝗈𝗋𝗍}$	$1$	$i\ge 0\wedge j\ge i$
$\mathrm{𝗆𝖾𝗋𝗀𝖾}$	$8$	$i\ge 0\wedge j\ge i$
$\mathrm{𝗆𝖾𝗋𝗀𝖾}$	$11$	$l\ge i\wedge l\le j+1$
$\mathrm{𝗆𝖾𝗋𝗀𝖾}$	$19$	$l\ge i\wedge l\le j+1$

Table 3. Table 3: Templates at Significant Labels

$𝖿$	$\ell$	$\eta (𝖿,\ell )$
$\mathrm{𝗆𝖾𝗋𝗀𝖾𝗌𝗈𝗋𝗍}$	$1$	$c_1\left(j-i+1\right)\ln \left(j-i+1\right)+c_2$
$\mathrm{𝗆𝖾𝗋𝗀𝖾}$	$8$	$c_3\left(j-i+1\right)+c_4$
$\mathrm{𝗆𝖾𝗋𝗀𝖾}$	$11$	$c_{5}l+c_{6}j+c_{7}i+c_8$
$\mathrm{𝗆𝖾𝗋𝗀𝖾}$	$19$	$c_{9}l+c_{10}j+c_{11}$

variable	value	variable	value
$c_1$	40.9650	$c_7$	-3
$c_2$	3	$c_8$	12
$c_3$	9	$c_9$	-3
$c_4$	6	$c_{10}$	3
$c_5$	-6	$c_{11}$	4
$c_6$	9

Equations

$$\left(1000-3000\cdot {\left(1/2\right)}^{1.6}\right)\cdot u-7\cdot n=$$

$$\frac{7}{2^{0.6}}\cdot \left(u-2^{0.6}\cdot n\right)+\frac{1000\cdot 2^{1.6}-3014}{2^{1.6}}\cdot \left(u-2^{1.6}\right)+\left(1000\cdot 2^{1.6}-3014\right)\cdot 1.$$

$$\mathfrak{e}={\sum }_i{c}_i\cdot g_i$$

$$\max\big{\{}\textstyle\sum_{j}\mathbf{1}_{\phi_{1j}}\cdot h_{1j},~{}\dots,~{}\textstyle\sum_{j}\mathbf{1}_{\phi_{mj}}\cdot h_{mj}\big{\}}$$

$$\forall \vec{x}\in {\mathbb{R}}^N.\left(\vec{x}\in \mathsf{Sat}(\Gamma )\to \widetilde{{\mathfrak{e}}^{\prime }}(\vec{x})\ge t_{{\mathfrak{e}}^{\prime }}\right)$$

$$\forall \vec{x}\in {\mathbb{R}}^N.\left[\vec{x}\in \mathsf{Sat}(\Gamma )\to \tilde{\mathfrak{e}}(\vec{x})-\left(r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}\cdot \widetilde{{\mathfrak{e}}^{\prime }}(\vec{x})+b_{\mathfrak{e},{\mathfrak{e}}^{\prime }}\right)\ge 0\right]\text{ and }$$

$$\forall \vec{x}\in {\mathbb{R}}^N.\left[\vec{x}\in \mathsf{Sat}(\Gamma )\to r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}\cdot \widetilde{{\mathfrak{e}}^{\prime }}(\vec{x})+b_{\mathfrak{e},{\mathfrak{e}}^{\prime }}\ge 1\right]$$

$$\forall \vec{x}\in {\mathbb{R}}^N.\left[\vec{x}\in \mathsf{Sat}(\Gamma )\to \left({\mathsf{r}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}\cdot \widetilde{{\mathfrak{e}}^{\prime }}(\vec{x})+{\mathsf{b}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}\right)-\tilde{\mathfrak{e}}(\vec{x})\ge 0\right]$$

$$u_{\mathfrak{e}}-\ln r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }-u_{{\mathfrak{e}}^{\prime }}+1_{b_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }<0}\cdot {\left(t_{{\mathfrak{e}}^{\prime }}+\frac{b_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}{r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}\right)}^{-1}\cdot \left(-\frac{b_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}{r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}\right)$$

$$\ln [[\mathfrak{e}]]$$

$$u_{{\mathfrak{e}}^{\prime }}+\ln {\mathsf{r}}_{\mathfrak{e},\mathfrak{e}}^{\ast }-u_{\mathfrak{e}}+1_{{\mathsf{b}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }\ge 0}\cdot t_{{\mathfrak{e}}^{\prime }}^{-1}\cdot \frac{b_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}{r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}$$

$$\ln [[\mathfrak{e}]]$$

$$t_{{\mathfrak{e}}^{\prime }}+\frac{{\mathsf{b}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}{{\mathsf{r}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}\ge 1$$

$$v_{\mathfrak{e}}-{\left(r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }\right)}^r\cdot \left(v_{{\mathfrak{e}}^{\prime }}+r\cdot \frac{b_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}{r_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}\cdot v_{{\mathfrak{e}}^{\prime }}^{\prime }\right)$$

$${[[\mathfrak{e}]]}^r$$

$${\left({\mathsf{r}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }\right)}^r\cdot \left(v_{{\mathfrak{e}}^{\prime }}+\left(1_{{\mathsf{b}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }\le 0}+1_{{\mathsf{b}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }>0}\cdot M^{r-1}\right)\cdot r\cdot \frac{{\mathsf{b}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}{{\mathsf{r}}_{\mathfrak{e},{\mathfrak{e}}^{\prime }}^{\ast }}\cdot v_{{\mathfrak{e}}^{\prime }}^{\prime }\right)-v_{\mathfrak{e}}$$

$${[[\mathfrak{e}]]}^r$$

$$g={\sum }_{i=1}^n{c}_i\cdot u_i$$

$$\frac{h\in \Gamma }{{⊢}_{1}h\ge 0}\frac{c\in \mathbb{R},c\ge 0}{{⊢}_{1}c\ge 0}\frac{{⊢}_{k}h\ge 0,c\in \mathbb{R},c\ge 0}{{⊢}_{k}c\cdot h\ge 0}$$

$$\frac{{⊢}_k{h}_1\ge 0,{⊢}_k{h}_2\ge 0}{{⊢}_k{h}_1+h_2\ge 0}\frac{{⊢}_{k_1}{h}_1\ge 0,{⊢}_{k_2}{h}_2\ge 0}{{⊢}_{k_1+k_2}{h}_1\cdot h_2\ge 0}.$$

$$⟨prog⟩::=⟨func⟩⟨prog⟩\mid ⟨func⟩$$

$$\displaystyle\langle\mathit{func}\rangle::=\,\langle\mathit{fname}\rangle\mbox{`$($'}\langle plist\rangle\mbox{`$)$'}\mbox{`$\{$'}\langle stmt\rangle\mbox{`$\}$'}$$

$$\displaystyle\langle plist\rangle::=\,\langle\mathit{pvar}\rangle\mid\langle\mathit{pvar}\rangle\mbox{`$,$'}\langle\mathit{plist}\rangle$$

$$\displaystyle\langle\mathit{stmt}\rangle::=\mbox{`{skip}'}\mid\langle\mathit{pvar}\rangle\,\mbox{`$:=$'}\,\langle\mathit{expr}\rangle$$

$$\displaystyle\mid\langle\mathit{fname}\rangle\mbox{`$($'}\langle\mathit{vlist}\rangle\mbox{`$)$'}$$

$$\mid \text{mbox}‘{if}^{\prime }⟨bexpr⟩\text{mbox}‘{then}^{\prime }⟨stmt⟩\text{mbox}‘{else}^{\prime }⟨stmt⟩\text{mbox}‘{fi}^{\prime }$$

$$\mid \text{mbox}‘{if}^{\prime }\star \text{mbox}‘{then}^{\prime }⟨stmt⟩\text{mbox}‘{else}^{\prime }⟨stmt⟩\text{mbox}‘{fi}^{\prime }$$

$$\mid \text{mbox}‘{while}^{\prime }⟨bexpr⟩\text{‘do’}⟨stmt⟩\text{‘od’}$$

$$\mid ⟨stmt⟩\text{‘;’}⟨stmt⟩$$

$$⟨expr⟩::=⟨int⟩\mid ⟨pvar⟩$$

$$\displaystyle\mid\langle\mathit{expr}\rangle\,\mbox{`$+$'}\,\langle\mathit{expr}\rangle\mid\langle\mathit{expr}\rangle\,\mbox{`$-$'}\,\langle\mathit{expr}\rangle$$

$$\displaystyle\mid\langle\mathit{int}\rangle\,\mbox{`$*$'}\,\langle\mathit{expr}\rangle\mid\mbox{`$\Big{\lfloor}$'}\frac{\langle\mathit{expr}\rangle}{\langle\mathit{nonzero}\rangle}\mbox{`$\Big{\rfloor}$'}$$

$$⟨vlist⟩::=⟨expr⟩\mid ⟨expr⟩\text{mbox}‘{,}^{\prime }⟨vlist⟩$$

$$\displaystyle\langle\mathit{literal}\rangle::=\langle\mathit{expr}\rangle\,\mbox{`$\leq$'}\,\langle\mathit{expr}\rangle\mid\langle\mathit{expr}\rangle\,\mbox{`$\geq$'}\,\langle\mathit{expr}\rangle$$

$$⟨bexpr⟩::=⟨literal⟩\mid \neg ⟨bexpr⟩$$

$$\mid ⟨bexpr⟩\text{mbox}‘{or}^{\prime }⟨bexpr⟩\mid ⟨bexpr⟩\text{mbox}‘{and}^{\prime }⟨bexpr⟩$$

$$\left(\nu \left[\mathfrak{e}/x\right]\right)(q)=\{\begin{array}{ll}\nu (q)& \text{mbox}ifq\in V^{\mathsf{f}}\backslash \{x\}\\ \mathfrak{e}(\nu )& \text{mbox}ifq=x\end{array}.$$

$$\nu [\mathsf{g},\{{\mathfrak{e}}_j{\}}_{1\le j\le k}](q):=\{\begin{array}{ll}{\mathfrak{e}}_j(\nu )& \text{mbox}ifq=q_j\text{mbox}forsomej\\ 0& \text{mbox}ifq\in V^{\mathsf{g}}\backslash \{q_1,\dots ,q_k\}\end{array}.$$

Full text

1 Introduction

Automated analysis to obtain quantitative performance characteristics of programs is a key feature of static analysis. Obtaining precise worst-case complexity bounds is a topic of both wide theoretical and practical interest. The manual proof of such bounds can be cumbersome as well as require mathematical ingenuity, e.g., the book The Art of Computer Programming by Knuth presents several mathematically involved methods to obtain such precise bounds [51]. The derivation of such worst-case bounds requires a lot of mathematical skills and is not an automated method. However, the problem of deriving precise worst-case bounds is of huge interest in program analysis: (a) first, in applications such as hard real-time systems, guarantees of worst-case behavior are required; and (b) the bounds are useful in early detection of egregious performance problems in large code bases. Works such as [35, 36, 39, 40] provide an excellent motivation for the study of automatic methods to obtain worst-case bounds for programs.

Given the importance of the problem of deriving worst-case bounds, the problem has been studied in various different ways.

WCET Analysis. The problem of worst-case execution time (WCET) analysis is a large field of its own, that focuses on (but is not limited to) sequential loop-free code with low-level hardware aspects [66]. 2. 2.

Resource Analysis. The use of abstract interpretation and type systems to deal with loop, recursion, data-structures has also been considered  [36, 1, 49], e.g., using linear invariant generation to obtain disjunctive and non-linear bounds [18], potential-based methods for handling recursion and inductive data structures [39, 40]. 3. 3.

Ranking Functions. The notion of ranking functions is a powerful technique for termination analysis of (recursive) programs [8, 9, 19, 57, 63, 24, 67, 60]. They serve as a sound and complete approach for proving termination of non-recursive programs [30], and they have also been extended as ranking supermatingales for analysis of probabilistic programs [12, 28, 15, 14].

Given the many results above, two aspects of the problem have not been addressed.

WCET Analysis of Recursive Programs through Ranking Functions. The use of ranking functions has been limited mostly to non-recursive programs, and their use to obtain worst-case bounds for recursive programs has not been explored in depth. 2. 2.

Efficient Methods for Precise Bounds. While previous works present methods for disjunctive polynomial bounds [36] (such as $\max(0,n)\cdot(1+max(n,m))$), or multivariate polynomial analysis [39], these works do not provide efficient methods to synthesize bounds such as $\mathcal{O}(n\log n)$ or $\mathcal{O}(n^{r})$, where $r$ is not an integer.

We address these two aspects, i.e., efficient methods for obtaining non-polynomial bounds such as $\mathcal{O}(n\log n)$, $\mathcal{O}(n^{r})$ for recursive programs, where $r$ is not an integer.

Our Contributions. Our main contributions are as follows:

First, we apply ranking functions to recursion, resulting in measure functions, and show that they provide a sound and complete method to prove termination and worst-case bounds of non-deterministic recursive programs. 2. 2.

Second, we present a sound approach for handling measure functions of specific forms. More precisely, we show that non-polynomial measure functions involving logarithm and exponentiation can be synthesized using linear programming through abstraction of logarithmic or exponentiation terms, Farkas’ Lemma, and Handelman’s Theorem. 3. 3.

A key application of our method is the worst-case analysis of recursive programs. Our procedure can synthesize non-polynomial bounds of the form $\mathcal{O}(n\log n)$, as well as $\mathcal{O}(n^{r})$, where $r$ is not an integer. We show the applicability of our technique to obtain worst-case complexity bounds for several classical recursive programs:

• •

For Merge-Sort [23, Chapter 2] and the divide-and-conquer algorithm for the Closest-Pair problem [23, Chapter 33], we obtain $\mathcal{O}(n\log n)$ worst-case bound, and the bounds we obtain are asymptotically optimal. Note that previous methods are either not applicable, or grossly over-estimate the bounds as $\mathcal{O}(n^{2})$.

• •

For Karatsuba’s algorithm for polynomial multiplication (cf. [51]) we obtain a bound of $\mathcal{O}(n^{1.6})$, whereas the optimal bound is $n^{\log_{2}3}\approx\mathcal{O}(n^{1.585})$, and for the classical Strassen’s algorithm for fast matrix multiplication (cf. [23, Chapter 4]) we obtain a bound of $\mathcal{O}(n^{2.9})$ whereas the optimal bound is $n^{\log_{2}7}\approx\mathcal{O}(n^{2.8074})$. Note that previous methods are either not applicable, or grossly over-estimate the bounds as $\mathcal{O}(n^{2})$ and $\mathcal{O}(n^{3})$, respectively. 4. 4.

We present experimental results to demonstrate the effectiveness of our approach.

Applicability. In general, our approach can be applied to (recursive) programs where the worst-case behaviour can be obtained by an analysis that involves only the structure of the program. For example, our approach cannot handle the Euclidean algorithm for computing the greatest common divisor of two given natural numbers, since the worst-case behaviour of this algorithm relies on Lamé’s Theorem [51].

Key Novelty. The key novelty of our approach is that we show how non-trivial non-polynomial worst-case upper bounds such as $\mathcal{O}(n\log n)$ and $\mathcal{O}(n^{r})$, where $r$ is non-integral, can be soundly obtained, even for recursive programs, using linear programming. Moreover, as our computational tool is linear programming, the approach we provide is also a relatively scalable one (see Remark 5).

2 Non-deterministic Recursive Programs

In this work, our main contributions involve a new approach for non-polynomial worst-case analysis of recursive programs. To focus on the new contributions, we consider a simple programming language for non-deterministic recursive programs.In our language, (a) all scalar variables hold integers, (b) all assignments to scalar variables are restricted to linear expressions with floored operation, and (c) we do not consider return statements. The reason to consider such a simple language is that (i) non-polynomial worst-case running time often involves non-polynomial terms over integer-valued variables (such as array length) only, (ii) assignments to variables are often linear with possible floored expressions (in e.g. divide-and-conquer programs) and (iii) return value is often not related to worst-case behaviour of programs.

For a set $A$, we denote by $|A|$ the cardinality of $A$ and $\mathbf{1}_{A}$ the indicator function on $A$. We denote by $\mathbb{N}$, $\mathbb{N}_{0}$, $\mathbb{Z}$, and $\mathbb{R}$ the sets of all positive integers, non-negative integers, integers, and real numbers, respectively. Below we fix a set $\mathcal{X}$ of scalar variables.

Arithmetic Expressions, Valuations, and Predicates. The set of (linear) arithmetic expressions $\mathfrak{e}$ over $\mathcal{X}$ is generated by the following grammar: $\mathfrak{e}::=c\mid x\mid\left\lfloor\frac{\mathfrak{e}}{c}\right\rfloor\mid\mathfrak{e}+\mathfrak{e}\mid\mathfrak{e}-\mathfrak{e}\mid c*\mathfrak{e}$ where $c\in\mathbb{Z}$ and $x\in\mathcal{X}$. Informally, (i) $\frac{\centerdot}{c}$ refers to division operation, (ii) $\lfloor\centerdot\rfloor$ refers to the floored operation, and (iii) $+,-,*$ refer to addition, subtraction and multiplication operation over integers, respectively. In order to make sure that division is well-defined, we stipulate that every appearance of $c$ in $\frac{\mathfrak{e}}{c}$ is non-zero. A valuation over $\mathcal{X}$ is a function $\nu$ from $\mathcal{X}$ into $\mathbb{Z}$. Informally, a valuation assigns to each scalar variable an integer. Under a valuation $\nu$ over $\mathcal{X}$, an arithmetic expression $\mathfrak{e}$ can be evaluated to an integer in the straightforward way. We denote by $\mathfrak{e}(\nu)$ the evaluation of $\mathfrak{e}$ under $\nu$. The set of propositional arithmetic predicates $\phi$ over $\mathcal{X}$ is generated by the following grammar: $\phi::=\mathfrak{e}\leq\mathfrak{e}\mid\mathfrak{e}\geq\mathfrak{e}\mid\neg\phi\mid\phi\wedge\phi\mid\phi\vee\phi$ where $\mathfrak{e}$ represents an arithmetic expression. The satisfaction relation $\models$ between valuations and propositional arithmetic predicates is defined in the straightforward way through evaluation of arithmetic expressions (cf. Appendix 0.B for details). For each propositional arithmetic predicate $\phi$, $\mathbf{1}_{\phi}$ is interpreted as the indicator function $\nu\mapsto\mathbf{1}_{\nu\models\phi}$ on valuations, where $\mathbf{1}_{\nu\models\phi}$ is $1$ if $\nu\models\phi$ and [math] otherwise.

Syntax of the Programming Language. Due to page limit, we present a brief description of our syntax. The syntax is essentially a subset of C programming language: in our setting, we have scalar variables which hold integers and function names which corresponds to functions (in programming-language sense); assignment statements are indicated by ‘$:=$’, whose left-hand-side is a scalar variable and whose right-hand-side is a linear arithmetic expression; ‘skip’ is the statement which does nothing; while-loops and conditional if-branches are indicated by ‘while’ and ‘if’ respectively, together with a propositional arithmetic predicate indicating the relevant condition (or guard); demonic non-deterministic branches are indicated by ‘if’ and ‘$\star$’; function declarations are indicated by a function name followed by a bracketed list of non-duplicate scalar variables, while function calls are indicated by a function name followed by a bracketed list of linear arithmetic expressions; each function declaration is followed by a curly-braced compound statement as function body; finally, a program is a sequence of function declarations with their function bodies. (cf. Appendix 0.C for details).

Statement Labeling. Given a recursive program in our syntax, we assign a distinct natural number (called label in our context) to every assignment/skip statement, function call, if/while-statement and terminal line in the program. Informally, each label serves as a program counter which indicates the next statement to be executed.

Semantics through CFGs. We use control-flow graphs (CFGs) to specify the semantics of recursive programs. Informally, a CFG specifies how values for scalar variables and the program counter change in a program.

Definition 1 (Control-Flow Graphs)

A control-flow graph (CFG) is a triple which takes the form $({\dagger})~{}\left(\mathit{F},\left\{\left(\mathit{L}^{\mathsf{f}},\mathit{L}_{\mathrm{b}}^{\mathsf{f}},\mathit{L}_{\mathrm{a}}^{\mathsf{f}},\mathit{L}_{\mathrm{c}}^{\mathsf{f}},\mathit{L}_{\mathrm{d}}^{\mathsf{f}},V^{\mathsf{f}},\ell_{\mathrm{in}}^{\mathsf{f}},\ell_{\mathrm{out}}^{\mathsf{f}}\right)\right\}_{\mathsf{f}\in\mathit{F}},\left\{{\rightarrow}_{\mathsf{f}}\right\}_{\mathsf{f}\in\mathit{F}}\right)$ where:

• •

$\mathit{F}$ is a finite set of function names;

• •

each $\mathit{L}^{\mathsf{f}}$ is a finite set of labels attached to the function name $\mathsf{f}$, which is partitioned into (i) the set $\mathit{L}_{\mathrm{b}}^{\mathsf{f}}$ of branching labels, (ii) the set $\mathit{L}_{\mathrm{a}}^{\mathsf{f}}$ of assignment labels, (iii) the set $\mathit{L}_{\mathrm{c}}^{\mathsf{f}}$ of call labels and (iv) the set $\mathit{L}_{\mathrm{d}}^{\mathsf{f}}$ of demonic non-deterministic labels;

• •

each $V^{\mathsf{f}}$ is the set of scalar variables attached to $\mathsf{f}$;

• •

each $\ell_{\mathrm{in}}^{\mathsf{f}}$ (resp. $\ell_{\mathrm{out}}^{\mathsf{f}}$) is the initial label (resp. terminal label) in $\mathit{L}^{\mathsf{f}}$;

• •

each ${\rightarrow}_{\mathsf{f}}$ is a relation whose every member is a triple of the form $(\ell,\alpha,\ell^{\prime})$ for which $\ell$ (resp. $\ell^{\prime}$) is the source label (resp. target label) of the triple such that $\ell\in\mathit{L}^{\mathsf{f}}$ (resp. $\ell^{\prime}\in\mathit{L}^{\mathsf{f}}$), and $\alpha$ is (i) either a propositional arithmetic predicate $\phi$ over $V^{\mathsf{f}}$ (as the set of scalar variables) if $\ell\in\mathit{L}_{\mathrm{b}}^{\mathsf{f}}$, (ii) or an update function from the set of valuations over $V^{\mathsf{f}}$ into the set of valuations over $V^{\mathsf{f}}$ if $\ell\in\mathit{L}_{\mathrm{a}}^{\mathsf{f}}$, (iii) or a pair $(\mathsf{g},h)$ with $\mathsf{g}\in\mathit{F}$ and $h$ being a value-passing function which maps every valuation over $V^{\mathsf{f}}$ to a valuation over $V^{\mathsf{g}}$ if $\ell\in\mathit{L}_{\mathrm{c}}^{\mathsf{f}}$, (iv) or $\star$ if $\ell\in\mathit{L}_{\mathrm{d}}^{\mathsf{f}}$.

W.l.o.g, we consider that all labels are natural numbers. We denote by $\mbox{\sl Val}_{\mathsf{f}}$ the set of valuations over $V^{\mathsf{f}}$, for each $\mathsf{f}\in\mathit{F}$. Informally, a function name $\mathsf{f}$, a label $\ell\in\mathit{L}^{\mathsf{f}}$ and a valuation $\nu\in\mbox{\sl Val}_{\mathsf{f}}$ reflects that the current status of a recursive program is under function name $\mathsf{f}$, right before the execution of the statement labeled $\ell$ in the function body named $\mathsf{f}$ and with values specified by $\nu$, respectively.

Example 1

We consider the running example in Figure 2 which abstracts the running time of Binary-Search. The CFG for this example is depicted in Figure 2. ∎

For a detailed description of CFG and transformation from recursive programs to CFGs, see Appendix 0.D. Based on CFG, the semantics models executions of a recursive program as runs, and is defined through the standard notion of call stack. Below we fix a recursive program $P$ and its CFG taking the form (${\dagger}$). We first define the notion of stack element and configurations which captures all information within a function call.

Stack Elements and Configurations. A stack element $\mathfrak{c}$ (of $P$) is a triple $(\mathsf{f},\ell,\nu)$ (treated as a letter) where $\mathsf{f}\in\mathit{F}$, $\ell\in\mathit{L}^{\mathsf{f}}$ and $\nu\in\mbox{\sl Val}_{\mathsf{f}}$; $\mathfrak{c}$ is non-terminal if $\ell\in\mathit{L}^{\mathsf{f}}\setminus\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$. A configuration (of $P$) is a finite word of non-terminal stack elements (including the empty word $\varepsilon$). Thus, a stack element $(\mathsf{f},\ell,\nu)$ specifies that the current function name is $\mathsf{f}$, the next statement to be executed is the one labelled with $\ell$ and the current valuation w.r.t $\mathsf{f}$ is $\nu$; a configuration captures the whole trace of the call stack.

Schedulers and Runs. To resolve non-determinism indicated by $\star$, we consider the standard notion of schedulers, which have the full ability to look into the whole history for decision. Formally, a scheduler $\pi$ is a function that maps every sequence of configurations ending in a non-deterministic location to the next configuration. A stack element $\mathfrak{c}$ (as the initial stack element) and a scheduler $\pi$ defines a unique infinite sequence $\{w_{j}\}_{j\in\mathbb{N}_{0}}$ of configurations as the execution starting from $\mathfrak{c}$ and under $\pi$, which is denoted as the run $\rho(\mathfrak{c},\pi)$. This defines the semantics of recursive programs.

We now define the notion of termination time which corresponds directly to the running time of a recursive program. In our setting, execution of every step takes one time unit.

Definition 2 (Termination Time)

For each stack element $\mathfrak{c}$ and each scheduler $\pi$, the termination time of the run $\rho(\mathfrak{c},\pi)=\{w_{j}\}_{j\in\mathbb{N}_{0}}$, denoted by $T(\mathfrak{c},\pi)$, is defined as $T(\mathfrak{c},\pi):=\min\{j\mid w_{j}=\varepsilon\}$ (i.e., the earliest time when the stack is empty) where $\min\emptyset:=\infty$. For each stack element $\mathfrak{c}$, the worst-case termination-time function $\overline{T}$ is a function on the set of stack elements defined by: $\overline{T}(\mathfrak{c}):=\sup\{T(\mathfrak{c},\pi)\mid\pi\mbox{ is a scheduler for }P\}$.

Thus $\overline{T}$ captures the worst-case behaviour of the recursive program $P$.

3 Measure Functions

In this section, we introduce the notion of measure functions for recursive programs. We show that measure functions are sound and complete for nondeterministic recursive programs and serve as upper bounds for the worst-case termination-time function. In the whole section, we fix a recursive program $P$ together with its CFG taking the form (${\dagger}$). We now present the standard notion of invariants which represent reachable stack elements. Due to page limit, we omit the intuitive notion of reachable stack elements. Informally, a stack element is reachable w.r.t an initial function name and initial valuations satisfying a prerequisite (as a propositional arithmetic predicate) if it can appear in the run under some scheduler (cf. Definition 7 for more details).

Definition 3 (Invariants)

A (linear) invariant $I$ w.r.t a function name $\mathsf{f}^{*}$ and a propositional arithmetic predicate $\phi^{*}$ over $V^{\mathsf{f^{*}}}$ is a function that upon any pair $(\mathsf{f},\ell)$ satisfying $\mathsf{f}\in\mathit{F}$ and $\ell\in\mathit{L}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, $I(\mathsf{f},\ell)$ is a propositional arithmetic predicate over $V^{\mathsf{f}}$ such that (i) $I(\mathsf{f},\ell)$ is without the appearance of floored expressions (i.e. $\lfloor\centerdot\rfloor$) and (ii) for all stack elements $(\mathsf{f},\ell,\nu)$ reachable w.r.t $\mathsf{f}^{*},\phi^{*}$, $\nu\models I(\mathsf{f},\ell)$. The invariant $I$ is in disjunctive normal form if every $I(\mathsf{f},\ell)$ is in disjunctive normal form.

Obtaining invariants automatically is a standard problem in programming languages, and several techniques exist (such as abstract interpretation [25] or Farkas’ Lemma [18]). In the rest of the section we fix a(n initial) function name $\mathsf{f}^{*}\in\mathit{F}$ and a(n initial) propositional arithmetic predicate $\phi^{*}$ over $V^{\mathsf{f^{*}}}$. For each $\mathsf{f}\in\mathit{F}$ and $\ell\in\mathit{L}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, we define $D_{\mathsf{f},\ell}$ to be the set of all valuations $\nu$ w.r.t $\mathsf{f}$ such that $(\mathsf{f},\ell,\nu)$ is reachable w.r.t $\mathsf{f}^{*},\phi^{*}$. Below we introduce the notion of measure functions.

Definition 4 (Measure Functions)

A measure function w.r.t $\mathsf{f}^{*},\phi^{*}$ is a function $g$ from the set of stack elements into $[0,\infty]$ such that for all stack elements $(\mathsf{f},\ell,\nu)$, the following conditions hold:

• •

C1: if $\ell=\ell_{\mathrm{out}}^{\mathsf{f}}$, then $g(\mathsf{f},\ell,\nu)=0$;

• •

C2: if $\ell\in\mathit{L}_{\mathrm{a}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, $\nu\in D_{\mathsf{f},\ell}$ and $(\ell,h,\ell^{\prime})$ is the only triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$ and update function $h$, then $g(\mathsf{f},\ell^{\prime},h(\nu))+1\leq g(\mathsf{f},\ell,\nu)$;

• •

C3: if $\ell\in\mathit{L}_{\mathrm{c}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, $\nu\in D_{\mathsf{f},\ell}$ and $(\ell,(\mathsf{g},h),\ell^{\prime})$ is the only triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$ and value-passing function $h$, then $1+g(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},h(\nu))+g(\mathsf{f},\ell^{\prime},\nu)\leq g(\mathsf{f},\ell,\nu)$;

• •

C4: if $\ell\in\mathit{L}_{\mathrm{b}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, $\nu\in D_{\mathsf{f},\ell}$ and $(\ell,\phi,\ell_{1}),(\ell,\neg\phi,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$, then $\mathbf{1}_{\nu\models\phi}\cdot g(\mathsf{f},\ell_{1},\nu)+\mathbf{1}_{\nu\models\neg\phi}\cdot g(\mathsf{f},\ell_{2},\nu)+1\leq g(\mathsf{f},\ell,\nu)$;

• •

C5: if $\ell\in\mathit{L}_{\mathrm{d}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, $\nu\in D_{\mathsf{f},\ell}$ and $(\ell,\star,\ell_{1}),(\ell,\star,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$, then $\max\{g(\mathsf{f},\ell_{1},\nu),g(\mathsf{f},\ell_{2},\nu)\}+1\leq g(\mathsf{f},\ell,\nu)$.

Intuitively, a measure function is a non-negative function whose values strictly decrease along the executions regardless of the choice of the demonic scheduler. By applying ranking functions to configurations, one can prove the following theorem stating that measure functions are sound and complete for the worst-case termination-time function. The technical proof of the theorem is put in Appendix 0.F and Appendix 0.G.

Theorem 3.1 (Soundness and Completeness)

(1) (Soundness). For all measure functions $g$ w.r.t $\mathsf{f}^{*},\phi^{*}$, it holds that for all valuations $\nu\in\mbox{\sl Val}_{\mathsf{\mathsf{f}^{*}}}$ such that $\nu\models\phi^{*}$, we have $\overline{T}(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)\leq g(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)$. (2) (Completeness). $\overline{T}$ is a measure function w.r.t $\mathsf{f}^{*},\phi^{*}$.

By Theorem 3.1, to obtain an upper bound on the worst-case termination-time function, it suffices to synthesize a measure function. Below we show that it suffices to synthesize measure functions at cut-points (which we refer as significant labels).

Definition 5 (Significant Labels)

Let $\mathsf{f}\in\mathit{F}$. A label $\ell\in\mathit{L}^{\mathsf{f}}$ is significant if either $\ell=\ell_{\mathrm{in}}^{\mathsf{f}}$ or $\ell$ is the initial label to some while-loop appearing in the function body of $\mathsf{f}$.

We denote by $\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ the set of significant locations in $\mathit{L}^{\mathsf{f}}$. Informally, a significant label is a label where valuations cannot be easily deduced from other labels, namely valuations at the start of the function-call and at the initial label of a while loop.

The Expansion Construction (from $g$ to $\widehat{g}$). Let $g$ be a function from $\left\{(\mathsf{f},\ell,\nu)\mid\mathsf{f}\in\mathit{F},\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}},\nu\in\mbox{\sl Val}_{\mathsf{f}}\right\}$ into $[0,\infty]$. One can obtain from $g$ a function $\widehat{g}$ from the set of all stack elements into $[0,\infty]$ in a straightforward way through iterated application of the equality forms of C1–C5 (cf. Appendix 0.H for details).

4 The Synthesis Algorithm

By Theorem 3.1, measure functions are a sound approach for upper bounds of the worst-case termination-time function, and hence synthesis of measure functions of specific forms provide upper bounds for worst-case behaviour of recursive programs. We first define the synthesis problem of measure functions and then present the synthesis algorithm, where the initial stack element is integrated into the input invariant. Informally, the input is a recursive program, an invariant for the program and technical parameters for the specific form of a measure function, and the output is a measure function if the algorithm finds one, and fail otherwise.

The RecTermBou Problem. The RecTermBou problem is defined as follows:

• •

Input: a recursive program $P$, an invariant $I$ in disjunctive normal form and a quadruple $(d,\mathrm{op},r,k)$ of technical parameters;

• •

Output: a measure function $h$ w.r.t the quadruple $(d,\mathrm{op},r,k)$.

The quadruple $(d,\mathrm{op},r,k)$ specifies the form of a measure function in the way that $d\in\mathbb{N}$ is the degree of the measure function to be synthesized, $\mathrm{op}\in\{\mathrm{log},\mathrm{exp}\}$ signals either logarithmic (when $\mathrm{op}=\log$) (e.g., $n\ln{n}$) or exponential (when $\mathrm{op}=\mathrm{exp}$) (e.g., $n^{1.6}$) measure functions, $r$ is a rational number greater than $1$ which specifies the exponent in the measure function (i.e., $n^{r}$) when $\mathrm{op}=\mathrm{exp}$ and $k\in\mathbb{N}$ is a technical parameter required by Theorem 4.3.

Remark 1

In the input for RecTermBou we fix the exponent $r$ when $\mathrm{op}=\mathrm{exp}$. However, iterating with binary search over an input bounded range we can obtain a measure function in the given range as precise as possible. Moreover, the invariants can be obtained automatically through e.g. [18]. ∎

We present our algorithm SynAlgo for synthesizing measure functions for the RecTermBou problem. The algorithm is designed to synthesize one function over valuations at each function name and appropriate significant labels so that C1–C5 are fulfilled. Due to page limit, we illustrate the main conceptual details of our algorithm (more details are relegated to Appendix 0.I). Below we fix an input to our algorithm.

Overview. We present the overview of our solution which has the following five steps.

Step 1. Since one key aspect of our result is to obtain bounds of the form $\mathcal{O}(n\log n)$ as well as $\mathcal{O}(n^{r})$, where $r$ is not an integer, we first consider general form of upper bounds that involve logarithm and exponentiation (Step 1(a)), and then consider templates with the general form of upper bounds for significant labels (Step 1(b)). 2. 2.

Step 2. The second step considers the template generated in Step 1 for significant labels and generate templates for all labels. This step is relatively straightforward. 3. 3.

Step 3. The third step establishes constraint triples according to the invariant given by the input and the template obtained in Step 2. This step is also straightforward. 4. 4.

Step 4. The fourth step is the significant step which involves transforming the constraint triples generated in Step 3 into ones without logarithmic and exponentiation terms. The first substep (Step 4(a)) is to consider abstractions of logarithmic, exponentiation, and floored expressions as fresh variables. The next step (Step 4(b)) requires to obtain linear constraints over the abstracted variables. We use Farkas’ lemma and Lagrange’s Mean-Value Theorem (LMVT) to obtain sound linear inequalities for those variables. 5. 5.

Step 5. The final step is to solve the unknown coefficients of the template from the constraint triples (without logarithm or exponentiation) obtained from Step 4. This requires the solution of positive polynomials over polyhedrons through the sound form of Handelman’s Theorem (Theorem 4.3) to transform into a linear program.

We first present an informal illustration of the key ideas through a simple example.

Example 2

Consider the task to synthesize a measure function for Karatsuba’s algorithm [51] for polynomial multiplication which runs in $c\cdot n^{1.6}$ steps, where $c$ is a coefficient to be synthesized and $n$ represents the maximal degree of the input polynomials and is a power of $2$. We describe informally how our algorithm tackles Karatsuba’s algorithm. Let $n$ be the length of the two input polynomials and $c\cdot n^{1.6}$ be the template. Since Karatsuba’s algorithm involves three sub-multiplications and seven additions/subtractions, the condition C3 becomes () $c\cdot n^{1.6}-3\cdot c\cdot\left(\frac{n}{2}\right)^{1.6}-7\cdot n\geq 0$ for all $n\geq 2$. The algorithm first abstracts $n^{1.6}$ as a stand-alone variable $u$. Then the algorithm generates the following inequalities through properties of exponentiation: (**) $u\geq 2^{1.6},u\geq 2^{0.6}\cdot n$. Finally, the algorithm transforms () into () $c\cdot u-3\cdot\left(\frac{1}{2}\right)^{1.6}\cdot c\cdot u-7\cdot n\geq 0$ and synthesizes a value for $c$ through Handelman’s Theorem to ensure that () holds under $n\geq 2$ and (**). One can verify that $c=1000$ is a feasible solution since

[TABLE]

Hence, Karatsuba’s algorithm runs in $\mathcal{O}(n^{1.6})$ time.∎

4.1 Step 1 of SynAlgo

Step 1(a): General Form of A Measure Function.

Extended Terms. In order to capture non-polynomial worst-case complexity of recursive programs, our algorithm incorporates two types of extensions of terms.

Logarithmic Terms. The first extension, which we call $\log{}$-extension, is the extension with terms from $\ln{x},\ln{(x-y+1)}$ where $x,y$ are scalar variables appearing in the parameter list of some function name and $\ln{(\centerdot)}$ refers to the natural logarithm function with base $e$. Our algorithm will take this extension when $\mathrm{op}$ is $\log$. 2. 2.

Exponentiation Terms. The second extension, which we call $\mathrm{exp}$-extension, is with terms from $x^{r},(x-y+1)^{r}$ where $x,y$ are scalar variables appearing in the parameter list of some function name. The algorithm takes this when $\mathrm{op}=\mathrm{exp}$.

The intuition is that $x$ (resp. $x-y+1$) may represent a positive quantity to be halved iteratively (resp. the length between array indexes $y$ and $x$).

General Form. The general form for any coordinate function $\eta(\mathsf{f},\ell,\centerdot)$ of a measure function $\eta$ (at function name $\mathsf{f}$ and $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$) is a finite sum

[TABLE]

where (i) each $c_{i}$ is a constant scalar and each $g_{i}$ is a finite product of no more than $d$ terms (i.e., with degree at most $d$) from scalar variables in $V^{\mathsf{f}}$ and logarithmic/exponentiation extensions (depending on $\mathrm{op}$), and (ii) all $g_{i}$’s correspond to all finite products of no more than $d$ terms. Analogous to arithmetic expressions, for any such finite sum $\mathfrak{e}$ and any valuation $\nu\in\mbox{\sl Val}_{\mathsf{f}}$, we denote by $\mathfrak{e}(\nu)$ the real number evaluated through replacing any scalar variable $x$ appearing in $\mathfrak{e}$ with $\nu(x)$, provided that $\mathfrak{e}(\nu)$ is well-defined.

Semantics of General Form. A finite sum $\mathfrak{e}$ at $\mathsf{f}$ and $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ in the form (1) defines a function $\llbracket\mathfrak{e}\rrbracket$ on $\mbox{\sl Val}_{\mathsf{f}}$ in the way that for each $\nu\in\mbox{\sl Val}_{\mathsf{f}}$: $\llbracket\mathfrak{e}\rrbracket(\nu):=\mathfrak{e}(\nu)$ if $\nu\models I(\mathsf{f},\ell)$, and $\llbracket\mathfrak{e}\rrbracket(\nu):=0$ otherwise. Note that in the definition of $\llbracket\mathfrak{e}\rrbracket$, we do not consider the case when $\log$ or exponentiation is undefined. However, we will see in Step 1(b) below that $\log{}$ or exponentiation will always be well-defined.

Step 1(b): Templates. As in all previous works (cf. [19, 57, 24, 67, 60, 12, 15, 39]), we consider a template for measure function determined by the triple $(d,\mathrm{op},r)$ from the input parameters. Formally, the template determined by $(d,\mathrm{op},r)$ assigns to every function name $\mathsf{f}$ and $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ an expression in the form (1) (with degree $d$ and extension option $\mathrm{op}$). Note that a template here only restricts (i) the degree and (ii) $\log$ or $\mathrm{exp}$ extension for a measure function, rather than its specific form. Although $r$ is fixed when $\mathrm{op}=\mathrm{exp}$, one can perform a binary search over a bounded range for a suitable or optimal $r$.

In detail, the algorithm sets up a template $\eta$ for a measure function by assigning to each function name $\mathsf{f}$ and significant label $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ an expression $\eta(\mathsf{f},\ell)$ in a form similar to (1), except for that $c_{i}$’s in (1) are interpreted as distinct template variables whose actual values are to be synthesized. In order to ensure that logarithm and exponentiation are well-defined over each $I(\mathsf{f},\ell)$, we impose the following restriction ($\S$) on our template:

(§) $\ln{x},x^{r}$ (resp. $\ln{(x-y+1)},(x-y+1)^{r}$) appear in $\eta(\mathsf{f},\ell)$ only when $x-1\geq 0$ (resp. $x-y\geq 0$) can be inferred from the invariant $I(\mathsf{f},\ell)$.

To infer $x-1\geq 0$ or $x-y\geq 0$ from $I(\mathsf{f},\ell)$, we utilize Farkas’ Lemma.

Theorem 4.1 (Farkas’ Lemma [27, 59])

Let $\mathbf{A}\in\mathbb{R}^{m\times n}$, $\mathbf{b}\in\mathbb{R}^{m}$, $\mathbf{c}\in\mathbb{R}^{n}$ and $d\in\mathbb{R}$. Assume that $\{\mathbf{x}\mid\mathbf{A}\mathbf{x}\leq\mathbf{b}\}\neq\emptyset$. Then $\{\mathbf{x}\mid\mathbf{A}\mathbf{x}\leq\mathbf{b}\}\subseteq\{\mathbf{x}\mid\mathbf{c}^{\mathrm{T}}\mathbf{x}\leq d\}$ iff there exists $\mathbf{y}\in\mathbb{R}^{m}$ such that $\mathbf{y}\geq\mathbf{0}$, $\mathbf{A}^{\mathrm{T}}\mathbf{y}=\mathbf{c}$ and $\mathbf{b}^{\mathrm{T}}\mathbf{y}\leq d$.

By Farkas’ Lemma, there exists an algorithm that infers whether $x-1\geq 0$ (or $x-y\geq 0$) holds under $I(\mathsf{f},\ell)$ in polynomial time through emptiness checking of polyhedra (cf. [58]) since $I(\mathsf{f},\ell)$ involves only linear (degree-$1$) polynomials in our setting.

Then $\eta$ naturally induces a function $\llbracket\eta\rrbracket$ from $\left\{(\mathsf{f},\ell,\nu)\mid\mathsf{f}\in\mathit{F},\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}},\nu\in\mbox{\sl Val}_{\mathsf{f}}\right\}$ into $[0,\infty]$ parametric over template variables such that $\llbracket\eta\rrbracket(\mathsf{f},\ell,\nu)={\llbracket}{\eta(\mathsf{f},\ell)}{\rrbracket}(\nu)$ for all appropriate stack elements $(\mathsf{f},\ell,\nu)$. Note that $\llbracket\eta\rrbracket$ is well-defined since logarithm and exponentiation is well-defined over satisfaction sets given by $I$.

4.2 Step 2 of SynAlgo

Step 2: Computation of $\widehat{\llbracket\eta\rrbracket}$. Let $\eta$ be the template constructed from Step 1. This step computes $\widehat{\llbracket\eta\rrbracket}$ from $\eta$ by the expansion construction of significant labels (Section 3) which transforms a function $g$ into $\widehat{g}$. Recall the function $\llbracket\mathfrak{e}\rrbracket$ for $\mathfrak{e}$ is defined in Step 1(a). Formally, based on the template $\eta$ from Step 1, the algorithm computes $\widehat{\llbracket\eta\rrbracket}$, with the exception that template variables appearing in $\eta$ are treated as undetermined constants. Then $\widehat{\llbracket\eta\rrbracket}$ is a function parametric over the template variables in $\eta$.

By an easy induction, each $\widehat{\llbracket\eta\rrbracket}(\mathsf{f},\ell,\centerdot)$ can be represented by an expression in the form:

[TABLE]

each $\phi_{ij}$ is a propositional arithmetic predicate over $V^{\mathsf{f}}$ such that for each $i$, $\bigvee_{j}\phi_{ij}$ is tautology and $\phi_{ij_{1}}\wedge\phi_{ij_{2}}$ is unsatisfiable whenever $j_{1}\neq j_{2}$, and 2. 2.

each $h_{ij}$ takes the form similar to (1) with the difference that (i) each $c_{i}$ is either a scalar or a template variable appearing in $\eta$ and (ii) each $g_{i}$ is a finite product whose every multiplicand is either some $x\in V^{\mathsf{f}}$, or some $\lfloor\mathfrak{e}\rfloor$ with $\mathfrak{e}$ being an instance of $\langle\mathit{expr}\rangle$, or some $\ln{\mathfrak{e}}$ (or $\mathfrak{e}^{r}$, depending on $\mathrm{op}$) with $\mathfrak{e}$ being an instance of $\langle\mathit{expr}\rangle$.

For this step we use the fact that all propositional arithmetic predicates can be put in disjunctive normal form. For detailed description see Appendix 0.I.

4.3 Step 3 of SynAlgo

This step generates constraint triples from $\widehat{\llbracket\eta\rrbracket}$ computed in Step 2. By applying non-negativity and C2-C5 to $\widehat{\llbracket\eta\rrbracket}$ (computed in Step 2), the algorithm establishes constraint triples which will be interpreted as universally-quantified logical formulas later.

Constraint Triples. A constraint triple is a triple $(\mathsf{f},\phi,\mathfrak{e})$ where (i) $\mathsf{f}\in\mathit{F}$, (ii) $\phi$ is a propositional arithmetic predicate over $V^{\mathsf{f}}$ which is a conjunction of atomic formulae of the form $\mathfrak{e}^{\prime}\geq 0$ with $\mathfrak{e}^{\prime}$ being an arithmetic expression, and (iii) $\mathfrak{e}$ is an expression taking the form similar to (1) with the difference that (i) each $c_{i}$ is either a scalar, or a template variable $c$ appearing in $\eta$, or its reverse $-c$, and (ii) each $g_{i}$ is a finite product whose every multiplicand is either some $x\in V^{\mathsf{f}}$, or some $\lfloor\mathfrak{e}\rfloor$ with $\mathfrak{e}$ being an instance of $\langle\mathit{expr}\rangle$, or some $\ln{\mathfrak{e}}$ (or $\mathfrak{e}^{r}$, depending on $\mathrm{op}$) with $\mathfrak{e}$ being an instance of $\langle\mathit{expr}\rangle$.

For each constraint triple $(\mathsf{f},\phi,\mathfrak{e})$, the function $\llbracket\mathfrak{e}\rrbracket$ on $\mbox{\sl Val}_{\mathsf{f}}$ is defined in the way such that each $\llbracket\mathfrak{e}\rrbracket(\nu)$ is the evaluation result of $\mathfrak{e}$ when assigning $\nu(x)$ to each $x\in V^{\mathsf{f}}$; under (§) (of Step 1(b)), logarithm and exponentiation will always be well-defined.

Semantics of Constraint Triples. A constraint triple $(\mathsf{f},\phi,\mathfrak{e})$ encodes the following logical formula: $\forall\nu\in\mbox{\sl Val}_{\mathsf{f}}.\left(\nu\models\phi\rightarrow\llbracket\mathfrak{e}\rrbracket(\nu)\geq 0\right)$ . Multiple constraint triples are grouped into a single logical formula through conjunction.

Step 3: Establishment of Constraint Triples. Based on $\widehat{\llbracket\eta\rrbracket}$ (computed in the previous step), the algorithm generates constraint triples at each significant label, then group all generated constraint triples together in a conjunctive way. To be more precise, at every significant label $\ell$ of some function name $\mathsf{f}$, the algorithm generates constraint triples through non-negativity of measure functions and conditions C2–C5; after generating the constraint triples for each significant label, the algorithm groups them together in the conjunctive fashion to form a single collection of constraint triples. For details procedure see Appendix 0.I.

Example 3

Consider our running example (cf. Example 1). Let the input quadruple be $(1,\log,-,1)$ and invariant (at label 1) be $n\geq 1$ (length of array should be positive). In Step 1, the algorithm assigns the template $\eta(\mathsf{f},1,n)=c_{1}\cdot n+c_{2}\cdot\ln n+c_{3}$ at label 1 and $\eta(\mathsf{f},4,n)=0$ at label 4. In Step 2, the algorithm computes template at other labels and obtains that $\eta(\mathsf{f},2,n)=1+c_{1}\cdot\left\lfloor{n}/{2}\right\rfloor+c_{2}\cdot\ln{\left\lfloor{n}/{2}\right\rfloor}+c_{3}$ and $\eta(\mathsf{f},3,n)=1$. In Step 3, the algorithm establishes the following three constraint triples $\mathfrak{q}_{1},\mathfrak{q}_{2},\mathfrak{q}_{3}$:

• •

$\mathfrak{q}_{1}:=(\mathsf{f},n-1\geq 0,c_{1}\cdot n+c_{2}\cdot\ln n+c_{3})$ from the logical formula $\forall n.(n\geq 1)\rightarrow c_{1}\cdot n+c_{2}\cdot\ln n+c_{3}\geq 0$ for non-negativity of measure functions;

• •

$\mathfrak{q}_{2}:=(\mathsf{f},n-1\geq 0\wedge 1-n\geq 0,c_{1}\cdot n+c_{2}\cdot\ln n+c_{3}-2)$ and $\mathfrak{q}_{3}:=(\mathsf{f},n-2\geq 0,c_{1}\cdot(n-\left\lfloor{n}/{2}\right\rfloor)+c_{2}\cdot(\ln n-\ln{\left\lfloor{n}/{2}\right\rfloor})-2$ from resp. logical formulae

• –

$\forall n.(n\geq 1\wedge n\leq 1)\rightarrow c_{1}\cdot n+c_{2}\cdot\ln n+c_{3}\geq 2$ and

• –

$\forall n.(n\geq 2)\rightarrow c_{1}\cdot n+c_{2}\cdot\ln n+c_{3}\geq c_{1}\cdot\left\lfloor{n}/{2}\right\rfloor+c_{2}\cdot\ln{\left\lfloor{n}/{2}\right\rfloor}+c_{3}+2$

for C4 (at label 1).∎

4.4 Step 4 of SynAlgo

Step 4: Solving Constraint Triples. To check whether the logical formula encoded by the generated constraint triples is valid, the algorithm follows a sound method which abstracts each multiplicand other than scalar variables in the form (2) as a stand-alone variable, and transforms the validity of the formula into a system of linear inequalities over template variables appearing in $\eta$ through Handelman’s Theorem and linear programming. The main idea is that the algorithm establishes tight linear inequalities for those abstraction variables by investigating properties for the abstracted arithmetic expressions, and use linear programming to solve the formula based on the linear inequalities for abstraction variables. We note that validity of such logical formulae are generally undecidable since they involve non-polynomial terms such as logarithm [32].

Below we describe how the algorithm transforms a constraint triple into one without logarithmic or exponentiation term. Given any finite set $\Gamma$ of polynomials over $n$ variables, we define $\mathsf{Sat}(\Gamma):=\left\{\vec{x}\in\mathbb{R}^{n}\mid f(\vec{x})\geq 0\mbox{ for all }f\in\Gamma\right\}$ . In the whole step, we let $(\mathsf{f},\phi,\mathfrak{e}^{*})$ be any constraint triple such that $\phi=\bigwedge_{j}\mathfrak{e}_{j}\geq 0$; moreover, we maintain a finite set $\Gamma$ of linear (degree-$1$) polynomials over scalar and freshly-added variables. Intuitively, $\Gamma$ is related to both the set of all $\mathfrak{e}_{j}$’s (so that $\mathsf{Sat}(\Gamma)$ is somehow the satisfaction set of $\phi$) and the finite subset of polynomials in Theorem 4.3.

Step 4(a): Abstraction of Logarithmic, Exponentiation, and Floored Expressions. The first sub-step involves the following computational steps, where Items 2-4 handle variables for abstraction, and Item 6 is approximation of floored expressions, and other steps are straightforward.

Initialization. First, the algorithm maintains a finite set of linear (degree-$1$) polynomials $\Gamma$ and sets it initially to the empty set. 2. 2.

Logarithmic, Exponentiation and Floored Expressions. Next, the algorithm computes the following subsets of $\langle\mathit{expr}\rangle$:

• •

\mathcal{E}_{L}:=\{\mathfrak{e}\mid\mbox{ \ln{\mathfrak{e}}$appears in$\mathfrak{e}^{*} (as sub-expression)}\} upon $\mathrm{op}=\log$.

• •

\mathcal{E}_{E}:=\{\mathfrak{e}\mid\mbox{ {\mathfrak{e}}^{r}$appears in$\mathfrak{e}^{*} (as sub-expression)}\} upon $\mathrm{op}=\mathrm{exp}$.

• •

\mathcal{E}_{F}:=\{\mathfrak{e}\mid\mbox{ {\mathfrak{e}}$appears in$\mathfrak{e}^{*}$and takes the form$\lfloor\frac{\centerdot}{c}\rfloor}\}.

Let $\mathcal{E}:=\mathcal{E}_{L}\cup\mathcal{E}_{E}\cup\mathcal{E}_{F}$. 3. 3.

Variables for Logarithmic, Exponentiation and Floored Expressions. Next, for each $\mathfrak{e}\in\mathcal{E}$, the algorithm establishes fresh variables as follows:

• •

a fresh variable $u_{\mathfrak{e}}$ which represents $\ln{\mathfrak{e}}$ for $\mathfrak{e}\in\mathcal{E}_{L}$;

• •

two fresh variables $v_{\mathfrak{e}},v^{\prime}_{\mathfrak{e}}$ such that $v_{\mathfrak{e}}$ indicates ${\mathfrak{e}}^{r}$ and $v^{\prime}_{\mathfrak{e}}$ for ${\mathfrak{e}}^{r-1}$ for $\mathfrak{e}\in\mathcal{E}_{E}$;

• •

a fresh variable $w_{\mathfrak{e}}$ indicating $\mathfrak{e}$ for $\mathfrak{e}\in\mathcal{E}_{F}$.

We note that $v^{\prime}_{\mathfrak{e}}$ is introduced in order to have a more accurate approximation for $v_{\mathfrak{e}}$ later. After this step, the algorithm sets $N$ to be the number of all variables (i.e., all scalar variables and all fresh variables added up to this point). In the rest of this section, we consider an implicit linear order over all scalar and freshly-added variables so that a valuation of these variables can be treated as a vector in $\mathbb{R}^{N}$. 4. 4.

Variable Substitution (from ${\mathfrak{e}}$ to $\widetilde{\mathfrak{e}}$). Next, for each $\mathfrak{e}$ which is either $\mathfrak{t}$ or some $\mathfrak{e}_{j}$ or some expression in $\mathcal{E}$, the algorithm computes $\tilde{\mathfrak{e}}$ as the expression obtained from $\mathfrak{e}$ by substituting (i) every possible $u_{\mathfrak{e}^{\prime}}$ for $\ln{\mathfrak{e}^{\prime}}$, (ii) every possible $v_{\mathfrak{e}^{\prime}}$ for ${\left(\mathfrak{e}^{\prime}\right)}^{r}$ and (iii) every possible $w_{\mathfrak{e}^{\prime}}$ for $\mathfrak{e}^{\prime}$ such that $\mathfrak{e}^{\prime}$ is a sub-expression of $\mathfrak{e}$ which does not appear as sub-expression in some other sub-expression $\mathfrak{e}^{\prime\prime}\in\mathcal{E}_{F}$ of $\mathfrak{e}$. From now on, any $\mathfrak{e}$ or $\widetilde{\mathfrak{e}}$ or is deemed as a polynomial over scalar and freshly-added variables. Then any $\mathfrak{e}(\vec{x})$ or $\widetilde{\mathfrak{e}}(\vec{x})$ is the result of polynomial evaluation under the correspondence between variables and coordinates of $\vec{x}$ specified by the linear order. 5. 5.

Importing $\phi$ into $\Gamma$. The algorithm adds all $\widetilde{\mathfrak{e}_{j}}$ into $\Gamma$. 6. 6.

Approximation of Floored Expressions. For each $\mathfrak{e}\in\mathcal{E}_{F}$ such that $\mathfrak{e}=\lfloor\frac{\mathfrak{e}^{\prime}}{c}\rfloor$, the algorithm adds linear constraints for $w_{\mathfrak{e}}$ recursively on the nesting depth of floor operation as follows.

• •

Base Step. If $\mathfrak{e}=\lfloor\frac{\mathfrak{e}^{\prime}}{c}\rfloor$ and $\mathfrak{e}^{\prime}$ involves no nested floored expression, then the algorithm adds into $\Gamma$ either (i) $\widetilde{\mathfrak{e}^{\prime}}-c\cdot w_{\mathfrak{e}}\mbox{ and }c\cdot w_{\mathfrak{e}}-\widetilde{\mathfrak{e}^{\prime}}+c-1$ when $c\geq 1$, which is derived from $\frac{\mathfrak{e}^{\prime}}{c}-\frac{c-1}{c}\leq\mathfrak{e}\leq\frac{\mathfrak{e}^{\prime}}{c}$ , or (ii)  $c\cdot w_{\mathfrak{e}}-\widetilde{\mathfrak{e}^{\prime}}\mbox{ and }\widetilde{\mathfrak{e}^{\prime}}-c\cdot w_{\mathfrak{e}}-c-1$ when $c\leq-1$, which follows from $\frac{\mathfrak{e}^{\prime}}{c}-\frac{c+1}{c}\leq\mathfrak{e}\leq\frac{\mathfrak{e}^{\prime}}{c}$ . Second, given the current $\Gamma$, the algorithm finds the largest constant $t_{\mathfrak{e}^{\prime}}$ through Farkas’ Lemma such that

[TABLE]

holds; if such $t_{\mathfrak{e}^{\prime}}$ exists, the algorithm adds the constraint $w_{\mathfrak{e}}\geq\left\lfloor\frac{t_{\mathfrak{e}^{\prime}}}{c}\right\rfloor$ into $\Gamma$.

• •

Recursive Step. If $\mathfrak{e}=\lfloor\frac{\mathfrak{e}^{\prime}}{c}\rfloor$ and $\mathfrak{e}^{\prime}$ involves some nested floored expression, then the algorithm proceeds almost in the same way as for the Base Step, except that $\widetilde{\mathfrak{e}^{\prime}}$ takes the role of $\mathfrak{e}^{\prime}$. (Note that $\widetilde{\mathfrak{e}^{\prime}}$ does not involve nested floored expresions.) 7. 7.

Emptiness Checking. The algorithm checks whether $\mathsf{Sat}(\Gamma)$ is empty or not in polynomial time in the size of $\Gamma$ (cf. [58]). If $\mathsf{Sat}(\Gamma)=\emptyset$, then the algorithm discards this constraint triple with no linear inequalities generated, and proceeds to other constraint triples; otherwise, the algorithm proceeds to the remaining steps.

Example 4

We continue with Example 3. In Step 4(a), the algorithm first establishes fresh variables $u:=\ln n$, $v:=\ln{\left\lfloor{n}/{2}\right\rfloor}$ and $w:=\left\lfloor{n}/{2}\right\rfloor$, then finds that (i) $n-2\cdot w\geq 0$, (ii) $2\cdot w-n+1\geq 0$ and (iii) $n-2\geq 0$ (as $\Gamma$) implies that $w-1\geq 0$. After Step 4(a), the constraint triples after variable substitution and their $\Gamma$’s are as follows:

• •

$\widetilde{\mathfrak{q}_{1}}=(\mathsf{f},n-1\geq 0,c_{1}\cdot n+c_{2}\cdot u+c_{3})$ and $\Gamma_{1}=\{n-1\}$;

• •

$\widetilde{\mathfrak{q}_{2}}=(\mathsf{f},n-1\geq 0\wedge 1-n\geq 0,c_{1}\cdot n+c_{2}\cdot u+c_{3}-2)$ and $\Gamma_{2}=\{n-1,1-n\}$;

• •

$\widetilde{\mathfrak{q}_{3}}:=(\mathsf{f},n-2\geq 0,c_{1}\cdot(n-w)+c_{2}\cdot(u-v)-2)$ and $\Gamma_{3}=\{n-2,n-2\cdot w,2\cdot w-n+1,w-1\}$. ∎

For the next sub-step we will use Lagrange’s Mean-Value Theorem (LMVT) to approximate logarithmic and exponentiation terms.

Theorem 4.2 (Lagrange’s Mean-Value Theorem [6, Chapter 6])

Let $f:[a,b]\rightarrow\mathbb{R}$  (for $a<b$) be a function continuous on $[a,b]$ and differentiable on $(a,b)$. Then there exists a real number $\xi\in(a,b)$ such that $f^{\prime}(\xi)=\frac{f(b)-f(a)}{b-a}$.

Step 4(b): Linear Constraints for Abstracted Variables. The second sub-step consists of the following computational steps which establish into $\Gamma$ linear constraints for logarithmic or exponentiation terms. We present the details for logarithm, while similar technical details for exponentiation terms are in Appendix 0.I. Below we denote by $\mathcal{E}^{\prime}$ either the set $\mathcal{E}_{L}$ when $\mathrm{op}=\log$ or $\mathcal{E}_{E}$ when $\mathrm{op}=\mathrm{exp}$. Recall the $\widetilde{\mathfrak{e}}$ notation is defined in the Variable Substitution (Item 4) of Step 4(a).

Lower-Bound for Expressions in $\mathcal{E}^{\prime}$. For each $\mathfrak{e}\in\mathcal{E}^{\prime}$, we find the largest constant $t_{\mathfrak{e}}\in\mathbb{R}$ such that the logical formula $\forall\vec{x}\in\mathbb{R}^{N}.\left(\vec{x}\in\mathsf{Sat}(\Gamma)\rightarrow\widetilde{\mathfrak{e}}(\vec{x})\geq t_{\mathfrak{e}}\right)$ holds, This can be solved by Farkas’ Lemma and linear programming, since $\widetilde{\mathfrak{e}}$ is linear. Note that as long as $\mathsf{Sat}(\Gamma)\neq\emptyset$, it follows from (§) (in Step 1(b)) that $t_{\mathfrak{e}}$ is well-defined (since $t_{\mathfrak{e}}$ cannot be arbitrarily large) and $t_{\mathfrak{e}}\geq 1$. 2. 2.

Mutual No-Smaller-Than Inequalities over $\mathcal{E}^{\prime}$. For each pair $(\mathfrak{e},\mathfrak{e}^{\prime})\in\mathcal{E}^{\prime}\times\mathcal{E}^{\prime}$ such that $\mathfrak{e}\neq\mathfrak{e}^{\prime}$, the algorithm finds real numbers $r_{\left(\mathfrak{e},\mathfrak{e}^{\prime}\right)},b_{(\mathfrak{e},\mathfrak{e}^{\prime})}$ through Farkas’ Lemma and linear programming such that (i) $r_{(\mathfrak{e},\mathfrak{e}^{\prime})}\geq 0$ and (ii) both the logical formulae

[TABLE]

[TABLE]

hold. The algorithm first finds the maximal value $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ over all feasible $(r_{\mathfrak{e},\mathfrak{e}^{\prime}},b_{\mathfrak{e},\mathfrak{e}^{\prime}})$’s, then finds the maximal $b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ over all feasible $(r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}},b_{\mathfrak{e},\mathfrak{e}^{\prime}})$’s. If such $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ does not exist, the algorithm simply leaves $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ undefined. Note that once $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ exists and $\mathsf{Sat}(\Gamma)\neq\emptyset$, then $b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ exists since $b_{\mathfrak{e},\mathfrak{e}^{\prime}}$ cannot be arbitrarily large once $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ is fixed. 3. 3.

Mutual No-Greater-Than Inequalities over $\mathcal{E}^{\prime}$. For each pair $(\mathfrak{e},\mathfrak{e}^{\prime})\in\mathcal{E}^{\prime}\times\mathcal{E}^{\prime}$ such that $\mathfrak{e}\neq\mathfrak{e}^{\prime}$, the algorithm finds real numbers $\mathsf{r}_{\left(\mathfrak{e},\mathfrak{e}^{\prime}\right)},\mathsf{b}_{(\mathfrak{e},\mathfrak{e}^{\prime})}$ through Farkas’ Lemma and linear programming such that (i) $\mathsf{r}_{(\mathfrak{e},\mathfrak{e}^{\prime})}\geq 0$ and (ii) the logical formula

[TABLE]

holds. The algorithm first finds the minimal value $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ over all feasible $(\mathsf{r}_{\mathfrak{e},\mathfrak{e}^{\prime}},\mathsf{b}_{\mathfrak{e},\mathfrak{e}^{\prime}})$’s, then finds the minimal $\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ over all feasible $(\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}},\mathsf{b}_{\mathfrak{e},\mathfrak{e}^{\prime}})$’s. If such $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ does not exists, the algorithm simply leaves $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ undefined. Note that once $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ exists and $\mathsf{Sat}(\Gamma)$ is non-empty, then $\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ exists since $\mathsf{b}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ cannot be arbitrarily small once $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ is fixed. 4. 4.

Constraints from Logarithm. For each variable $u_{\mathfrak{e}}$, the algorithm adds into $\Gamma$ first the polynomial expression $\widetilde{\mathfrak{e}}-\left(\mathbf{1}_{t_{\mathfrak{e}}\leq e}\cdot e+\mathbf{1}_{t_{\mathfrak{e}}>e}\cdot\frac{t_{\mathfrak{e}}}{\ln t_{\mathfrak{e}}}\right)\cdot u_{\mathfrak{e}}$ from the fact that the function $z\mapsto\frac{z}{\ln{z}}$ ($z\geq 1$) has global minima at $e$ (so that the inclusion of this polynomial expression is sound), and then the polynomial expression $u_{\mathfrak{e}}-\ln{t_{\mathfrak{e}}}$ due to the definition of $t_{\mathfrak{e}}$. 5. 5.

Constraints from Exponentiation. For each variable $v_{\mathfrak{e}}$, the algorithm adds into $\Gamma$ polynomial expressions $v_{\mathfrak{e}}-t_{\mathfrak{e}}^{r-1}\cdot\widetilde{\mathfrak{e}}$ and $v_{\mathfrak{e}}-t_{\mathfrak{e}}^{r}$ due to the definition of $t_{\mathfrak{e}}$. And for each variable $v^{\prime}_{\mathfrak{e}}$, the algorithm adds (i) $v^{\prime}_{\mathfrak{e}}-t^{r-1}_{\mathfrak{e}}$ and (ii) either $v^{\prime}_{\mathfrak{e}}-t^{r-2}_{\mathfrak{e}}\cdot\tilde{\mathfrak{e}}$ when $r\geq 2$ or $\widetilde{\mathfrak{e}}-t^{2-r}_{\mathfrak{e}}\cdot v^{\prime}_{\mathfrak{e}}$ when $1<r<2$. 6. 6.

Mutual No-Smaller-Than Inequalities over $u_{\mathfrak{e}}$’s. For each pair $(\mathfrak{e},\mathfrak{e}^{\prime})\in\mathcal{E}^{\prime}\times\mathcal{E}^{\prime}$ such that $\mathfrak{e}\neq\mathfrak{e}^{\prime}$ and $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}},b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ are successfully found and $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}>0$, the algorithm adds

[TABLE]

into $\Gamma$. This is due to the fact that $\llbracket\mathfrak{e}\rrbracket-\left(r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\cdot\llbracket\mathfrak{e}^{\prime}\rrbracket+b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\right)\geq 0$ implies the following:

[TABLE]

where the last step is obtained from LMVT (Theorem 4.2) and by distinguishing whether $b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\geq 0$ or not, using the fact that the derivative of the natural-logarithm is the reciprocal function. Note that one has $t_{\mathfrak{e}^{\prime}}+\frac{b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}}{r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}}\geq 1$ due to the maximal choice of $t_{\mathfrak{e}^{\prime}}$. 7. 7.

Mutual No-Greater-Than Inequalities over $u_{\mathfrak{e}}$’s. For each pair $(\mathfrak{e},\mathfrak{e}^{\prime})\in\mathcal{E}^{\prime}\times\mathcal{E}^{\prime}$ such that $\mathfrak{e}\neq\mathfrak{e}^{\prime}$ and $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}},\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ are successfully found and $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}>0$, the algorithm adds

[TABLE]

into $\Gamma$. This is because $\left(\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\cdot\llbracket\mathfrak{e}^{\prime}\rrbracket+\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\right)-\llbracket\mathfrak{e}\rrbracket\geq 0$ implies

[TABLE]

where the last step is obtained from Lagrange’s Mean-Value Theorem and by distinguishing whether $\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\geq 0$ or not. Note that one has

[TABLE]

due to the maximal choice of $t_{\mathfrak{e}^{\prime}}$ and the fact that $\widetilde{\mathfrak{e}}$ (as a polynomial function) is everywhere greater than or equal to $1$ under $\mathsf{Sat}(\Gamma)$ (cf. (§)). 8. 8.

Mutual No-Smaller-Than Inequalities over $v_{\mathfrak{e}}$’s. For each pair of variables of the form $(v_{\mathfrak{e}},v_{\mathfrak{e}^{\prime}})$ such that $\mathfrak{e}\neq\mathfrak{e}^{\prime}$, $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}},b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ are successfully found and $r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}>0,b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\geq 0$, the algorithm adds

[TABLE]

into $\Gamma$. This is due to the fact that $\llbracket\mathfrak{e}\rrbracket-\left(r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\cdot\llbracket\mathfrak{e}^{\prime}\rrbracket+b^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\right)\geq 0$ implies

[TABLE]

where the last step is obtained from Lagrange’s Mean-Value Theorem. 9. 9.

Mutual No-Greater-Than Inequalities over $v_{\mathfrak{e}}$’s. For each pair of variables of the form $(v_{\mathfrak{e}},v_{\mathfrak{e}^{\prime}})$ such that $\mathfrak{e}\neq\mathfrak{e}^{\prime}$, $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}},\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}$ are successfully found and $\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}>0,\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\geq 0$, the algorithm adds

[TABLE]

into $\Gamma$, where $M:=\frac{\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}}{\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\cdot t_{\mathfrak{e}^{\prime}}}+1$. This is due to the fact that $\left(\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\cdot\llbracket\mathfrak{e}^{\prime}\rrbracket+\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}\right)-\llbracket\mathfrak{e}\rrbracket\geq 0$ implies

[TABLE]

where the last step is obtained from Lagrange’s Mean-Value Theorem and the fact that $\llbracket\mathfrak{e}^{\prime}\rrbracket\geq t_{\mathfrak{e}^{\prime}}$ implies $\llbracket\mathfrak{e}^{\prime}\rrbracket+\frac{\mathsf{b}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}}{\mathsf{r}^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}}\leq M\cdot\llbracket\mathfrak{e}^{\prime}\rrbracket$.

Although in Item 4 and Item 6 above, we have logarithmic terms such as $\ln t_{\mathfrak{e}}$ and $\ln{r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}}$, both $t_{\mathfrak{e}}$ and ${r^{*}_{\mathfrak{e},\mathfrak{e}^{\prime}}}$ are already determined constants, hence their approximations can be used. After Step 4, the constraint triple $(\mathsf{f},\phi,\mathfrak{e}^{*})$ is transformed into $(\mathsf{f},\bigwedge_{h\in\Gamma}h\geq 0,\widetilde{\mathfrak{e}^{*}})$.

Example 5

We continue with Example 4. In Step 4(b), the algorithm establishes the following non-trivial inequalities:

• •

(From Item 2,3 in Step 4(b) for $\widetilde{\mathfrak{q}_{3}}$) $w\geq 0.5\cdot n-0.5,w\leq 0.5\cdot n$ and $n\geq 2\cdot w,n\leq 2\cdot w+1$;

• •

(From Item 4 in Step 4(b) for $\widetilde{\mathfrak{q}_{1}},\widetilde{\mathfrak{q}_{2}}$) $n-e\cdot u\geq 0$ and $u\geq 0$;

• •

(From Item 4 in Step 4(b) for $\widetilde{\mathfrak{q}_{3}}$) $n-e\cdot u\geq 0,u-\ln{2}\geq 0$ and $w-e\cdot v\geq 0,v\geq 0$;

• •

(From Item 6,7 in Step 4(b) for $\widetilde{\mathfrak{q}_{3}}$) $u-v-\ln{2}\geq 0$ and $v-u+\ln{2}+\frac{1}{2}\geq 0$.

After Step 4(b), $\Gamma_{i}$’s ($1\leq i\leq 3$) are updated as follows:

• •

$\Gamma_{1}=\{n-1,n-e\cdot u,u\}$ and $\Gamma_{2}=\{n-1,1-n,n-e\cdot u,u\}$;

• •

$\Gamma_{3}=\{n-2,n-2\cdot w,2\cdot w-n+1,w-1,n-e\cdot u,u-\ln{2},w-e\cdot v,v,u-v-\ln{2},v-u+\ln{2}+\frac{1}{2}\}$.∎

Remark 2

The key difficulty is to handle logarithmic and exponentiation terms. In Step 4(a) we abstract such terms with fresh variables and perform sound approximation of floored expressions. In Step 4(b) we use Farkas’ Lemma and LMVT to soundly transform logarithmic or exponentiation terms to polynomials. ∎

Remark 3

The aim of Step 4(b) is to approximate logarithmic and exponentiation terms by linear inequalities they satisfy. In the final step, those linear inequalities suffice to solve our problem. As to extensibility, Step 4(b) may be extended to other non-polynomial terms by constructing similar linear inequalities they satisfy.∎

4.5 Step 5 of SynAlgo

This step is to solve the template variables in the template established in Step 1, based on the sets $\Gamma$ computed in Step 4. For this step, we use Handelman’s Theorem.

Definition 6 (Monoid)

Let $\Gamma$ be a finite subset of some polynomial ring ${\mathfrak{R}}{\left[x_{1},\dots,x_{m}\right]}$ such that all elements of $\Gamma$ are polynomials of degree $1$. The monoid of $\Gamma$ is defined by: $\mbox{\sl Monoid}(\Gamma):=\left\{\prod_{i=1}^{k}h_{i}\mid k\in\mathbb{N}_{0}\mbox{ and }h_{1},\dots,h_{k}\in\Gamma\right\}$  .

Theorem 4.3 (Handelman’s Theorem [37])

Let ${\mathfrak{R}}{\left[x_{1},\dots,x_{m}\right]}$ be the polynomial ring with variables $x_{1},\dots,x_{m}$ (for $m\geq 1$). Let $g\in{\mathfrak{R}}{\left[x_{1},\dots,x_{m}\right]}$ and $\Gamma$ be a finite subset of ${\mathfrak{R}}{\left[x_{1},\dots,x_{m}\right]}$ such that all elements of $\Gamma$ are polynomials of degree $1$. If (i) the set $\mathsf{Sat}(\Gamma)$ is compact and non-empty and (ii) $g(\vec{x})>0$ for all $\vec{x}\in\mathsf{Sat}(\Gamma)$, then

[TABLE]

for some $n\in\mathbb{N}$, non-negative real numbers $c_{1},\dots,c_{n}\geq 0$ and $u_{1},\dots,u_{n}\in\mbox{\sl Monoid}(\Gamma)$.

Basically, Handelman’s Theorem gives a characterization of positive polynomials over polytopes. In this paper, we concentrate on Eq. (3) which provides a sound form for a non-negative polynomial over a general (i.e. possibly unbounded) polyhedron. The following proposition shows that Eq. (3) encompasses a simple proof system for non-negative polynomials over polyhedra.

Proposition 1

Let $\Gamma$ be a finite subset of some polynomial ring ${\mathfrak{R}}{\left[x_{1},\dots,x_{m}\right]}$ such that all elements of $\Gamma$ are polynomials of degree $1$. Let the collection of deduction systems $\{\vdash_{k}\}_{k\in\mathbb{N}}$ be generate by the following rules:

[TABLE]

Then for all $k\in\mathbb{N}$ and polynomials $g\in{\mathfrak{R}}{\left[x_{1},\dots,x_{m}\right]}$, if $\vdash_{k}g\geq 0$ then $g=\sum_{i=1}^{n}c_{i}\cdot u_{i}$ for some $n\in\mathbb{N}$, non-negative real numbers $c_{1},\dots,c_{n}\geq 0$ and $u_{1},\dots,u_{n}\in\mbox{\sl Monoid}(\Gamma)$ such that every $u_{i}$ is a product of no more than $k$ polynomials in $\Gamma$.

Proof

By an easy induction on $k$.∎

Step 5: Solving Unknown Coefficients in the Template. Now we use the input parameter $k$ as the maximal number of multiplicands in each summand at the right-hand-side of Eq. (3). For any constraint triple $(\mathsf{f},\phi,\mathfrak{e}^{*})$ which is generated in Step 3 and passes the emptiness checking in Item 7 of Step 4(a), the algorithm performs the following steps.

Preparation for Eq. (3). The algorithm reads the set $\Gamma$ for $(\mathsf{f},\phi,\mathfrak{e}^{*})$ computed in Step 4, and computes $\widetilde{\mathfrak{e}^{*}}$ from Item 4 of Step 4(a). 2. 2.

Application of Handelman’s Theorem. First, the algorithm establishes a fresh coefficient variable $\lambda_{h}$ for each polynomial $h$ in $\mbox{Monoid}(\Gamma)$ with no more than $k$ multiplicands from $\Gamma$. Then, the algorithm establishes linear equalities over coefficient variables $\lambda_{h}$’s and template variables in the template $\eta$ established in Step 1 by equating coefficients of the same monomials at the left- and right-hand-side of the following polynomial equality $\widetilde{\mathfrak{\mathfrak{e}^{*}}}=\sum_{h}\lambda_{h}\cdot h$ . Second, the algorithm incorporates all constraints of the form $\lambda_{h}\geq 0$.

Then the algorithm collects all linear equalities and inequalities established in Item 2 above conjunctively as a single system of linear inequalities and solves it through linear-programming algorithms; if no feasible solution exists, the algorithm fails without output, otherwise the algorithm outputs the function $\widehat{\llbracket\eta\rrbracket}$ where all template variables in the template $\eta$ are resolved by their values in the solution. We now state the soundness of our approach for synthesis of measure functions (proof in Appendix 0.I).

Theorem 4.4

Our algorithm, SynAlgo, is a sound approach for the RecTermBou problem, i.e., if SynAlgo succeeds to synthesize a function $g$ on $\left\{(\mathsf{f},\ell,\nu)\mid\mathsf{f}\in\mathit{F},\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}},\nu\in\mbox{\sl Val}_{\mathsf{f}}\right\}$, then $\widehat{g}$ is a measure function and hence an upper bound on the termination-time function.

Remark 4

While Step 4 transforms logarithmic and exponentiation terms to polynomials, we need in Step 5 a sound method to solve polynomials with linear programming. We achieve this with Handelman’s Theorem. ∎

Example 6

Continue with Example 5. In the final step (Step 5), the unknown coefficients $c_{i}$’s ($1\leq i\leq 3$) are to be resolved through (3) so that logical formulae encoded by $\widetilde{\mathfrak{q}_{i}}$’s are valid (w.r.t updated $\Gamma_{i}$’s). Since to present the whole technical detail would be too cumbersome, we present directly a feasible solution for $c_{i}$’s and how they fulfill (3). Below we choose the solution that $c_{1}=0$, $c_{2}=\frac{2}{\ln{2}}$ and $c_{3}=2$. Then we have that

• •

(From $\widetilde{\mathfrak{q}_{1}}$) $c_{2}\cdot u+c_{3}=\lambda_{1}\cdot u+\lambda_{2}$ where $\lambda_{1}:=\frac{2}{\ln{2}}$ and $\lambda_{2}:=2$;

• •

(From $\widetilde{\mathfrak{q}_{2}}$) $c_{2}\cdot u+c_{3}-2=\lambda_{1}\cdot u$;

• •

(From $\widetilde{\mathfrak{q}_{3}}$) $c_{2}\cdot(u-v)-2=\lambda_{1}\cdot(u-v-\ln{2})$.

Hence by Theorem 3.1, $\overline{T}(\mathsf{f},1,n)\leq\eta(\mathsf{f},1,n)=\frac{2}{\ln{2}}\cdot\ln{n}+2$. It follows that Binary-Search runs in $\mathcal{O}(\log{n})$ in worst-case. ∎

Remark 5

We remark two aspects of our algorithm.

Scalability. Our algorithm only requires solving linear inequalities. Since linear-programming solvers have been widely studied and experimented, the scalability of our approach directly depends on the linear-programming solvers. Hence the approach we present is a relatively scalable one. 2. 2.

Novelty. A key novelty of our approach is to obtain non-polynomial bounds (such as $\mathcal{O}(n\log n)$ , $\mathcal{O}(n^{r})$, where $r$ is not integral) through linear programming. The novel technical steps are: (a) use of abstraction variables; (b) use of LMVT and Farkas’ lemma to obtain sound linear constraints over abstracted variables; and (c) use of Handelman’s Theorem to solve the unknown coefficients in polynomial time. ∎

5 Experimental Results

For worst-case upper bounds of non-trivial form, we consider four classical examples.

Merge-Sort and Closest-Pair. We consider the classical Merge-Sort problem [23, Chapter 2] and the closest pair problem consider a set of $n$ two-dimensional points and asks for the pair of points that have shortest Euclidean distance between them (cf. [23, Chapter 33]) (see Appendix 0.K for the pseudo-code). For both problems we obtain an $\mathcal{O}(n\log n)$ bound.

Strassen’s Algorithm. We consider one of the classic sub-cubic algorithm for Matrix multiplication. The Strassen algorithm (cf. [23, Chapter 4]) has a worst-case running time of $n^{\log_{2}7}$. We present the pseudo-code of Strassen’s algorithm in our programming language in Appendix 0.K. Using a template with $n^{2.9}$, our algorithm synthesizes a measure function.

Karatsuba’s Algorithm. We consider two polynomials $p_{1}=a_{0}+a_{1}x+a_{2}x^{2}+\ldots+a_{n}x^{n-1}$ and $p_{2}=b_{0}+b_{1}x+b_{2}x^{2}+\ldots+b_{n}x^{n-1}$, where the coefficients $a_{i}$’s and $b_{i}$’s are represented as arrays. The computational problem asks to compute the coefficients of the polynomial obtained by multiplication of $p_{1}$ and $p_{2}$, and considers that $n$ is a power of 2. While the most naive algorithm is quadratic, Karatsuba’s algorithm (cf. [51]) is a classical sub-quadratic algorithm for the problem with running time $n^{\log_{2}3}$. We present the pseudo-code Karatsuba’s algorithm in our programming language in Appendix 0.K. Using a template with $n^{1.6}$, our algorithm synthesizes a measure function (basically, using constraints as illustrated in Example 2).

The above four examples show that our sound approach can synthesize non-trivial worst-case complexity bounds for several classical algorithms.

Invariants. In the experiments we derive simple invariants from the programs directly from the prerequisites of procedures and guards of while-loops. Alternatively, they can be derived automatically using [18].

Results. Below we present experimental results on the examples explained above. We implement our algorithm that basically generates a set of linear constraints, where we use lp_solve [55] for solving linear programs. Our experimental results are presented in Table 1, where all numbers are rounded to $10^{-2}$ and $n$ represents the input length. All results were obtained on an Intel i3-4130 CPU 3.4 GHz 8 GB of RAM.

6 Related Work

In this section we discuss the related work. The termination of recursive programs or other temporal properties has already been extensively studied [20, 52, 22, 65, 26, 54, 53, 21, 5]. Our work is most closely related to automatic amortized analysis [41, 42, 43, 44, 45, 50, 49, 39, 31, 62, 4], as well as the SPEED project [35, 36, 34]. There are two key differences of our methods as compared to previous works. First, our methods are based on extension of ranking functions to non-deterministic recursive programs, whereas previous works either use potential functions, abstract interpretation, or size-change. Second, while none of the previous methods can derive non-polynomial bounds such as $\mathcal{O}(n^{r})$, where $r$ is not an integer, our approach gives an algorithm to derive such non-polynomial bounds, and surprisingly using linear programming.

The approach of recurrence relations for worst-case analysis is explored in [33, 29, 1, 2, 3]. A related result is by Albert et al. [2] who considered using evaluation trees for solving recurrence relations, which can derive the worst-case bound for Merge-Sort. Another approach through theorem proving is explored in [64]. The approach is to iteratively generate control-flow paths and then to obtain worst-case bounds over generated paths through theorem proving (with arithmetic theorems).

Ranking functions for intra-procedural analysis has been widely studied [8, 9, 19, 57, 63, 24, 67, 60]. Most works have focused on linear or polynomial ranking functions [19, 57, 63, 24, 67, 60]. Such approach alone can only derive polynomial bounds for programs. When integrated with evaluation trees, polynomial ranking functions can derive exponential bounds such as $\mathcal{O}(2^{n})$ [10]. In contrast, we directly synthesize non-polynomial ranking functions without the help of evaluation trees. Ranking functions have been extended to ranking supermartingales [12, 28, 15, 14, 13, 16] for probabilistic programs without recursion. These works cannot derive non-polynomial bounds.

Several other works present proof rules for deterministic programs [38] as well as for probabilistic programs [48, 56]. None of these works can be automated. Other related approaches are sized types [17, 46, 47], and polynomial resource bounds [61]. Again none of these approaches can yield bounds like $\mathcal{O}(n\log n)$ or $\mathcal{O}(n^{r})$, for $r$ non-integral.

Below we compare three most related works  [2, 10, 34].

Comparison with [2]. First, [2] uses synthesis of linear ranking functions in order to bound the number of nodes or the height of an evaluation tree for a cost relation system. We use expression abstraction to synthesize non-linear bounds. Second, [2] uses branching factor of a cost relation system to bound the number of nodes, which typically leads to exponential bounds. Our approach produces efficient bounds. Third, [2] treats Merge-sort in a very specific way: first, there is a ranking function with a discount-factor 2 to bound the height of an evaluation tree logarithmically, then there is a linear bound for levels in an evaluation tree which does not increase when the levels become deeper, and multiplying them together produces $\mathcal{O}(n\log n)$ bound. We do not rely on these heuristics. Finally, [2] is not applicable to non-direct-recursive cost relations, while our approach is applicable to all recursive programs.

Comparison with [10]. To derive non-polynomial bounds, [10] integrate polynomial ranking functions with evaluation trees for recursive programs so that exponential bounds such as $\mathcal{O}(2^{n})$ can be derived for Fibonacci numbers. In contrast, we directly synthesize non-polynomial ranking functions without the help of evaluation trees.

Comparison with [34]. [34] generates bounds through abstract interpretation using inference systems over expression abstraction with logarithm, maximum, exponentiation, etc. In contrast, we employ different method through ranking functions, also with linear-inequality system over expression abstraction with logarithm and exponentiation. The key difference w.r.t expression abstraction is that [34] handles in extra maximum and square root, while we consider in extra floored expressions and finer linear inequalities between e.g., $\log n,\log(n+1)$ or $n^{1.6},(n+1)^{1.6}$ through Lagrange’s Mean-Value Theorem.

7 Conclusion

In this paper, we developed an approach to obtain non-polynomial worst-case bounds for recursive programs through (i) abstraction of logarithmic and exponentiation terms and (ii) Farkas’ Lemma, LMVT, and Handelman’s Theorem. Moreover our approach obtains such bounds using linear programming, which thus is an efficient approach. Our approach obtains non-trivial worst-case complexity bounds for classical recursive programs: $\mathcal{O}(n\log{n})$-complexity for both Merge-Sort and the divide-and-conquer Closest-Pair algorithm, $\mathcal{O}(n^{1.6})$ for Karatsuba’s algorithm for polynomial multiplication, and $\mathcal{O}(n^{2.9})$ for Strassen’s algorithm for matrix multiplication. The bounds we obtain for Karatsuba’s and Strassen’s algorithm are close to the optimal bounds known. An interesting future direction is to extend our technique to data-structures. Another future direction is to investigate the application of our approach to invariant generation.

Acknowledgements

We thank all reviewers for valuable comments. The research is partially supported by Vienna Science and Technology Fund (WWTF) ICT15-003, Austrian Science Fund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), the Natural Science Foundation of China (NSFC) under Grant No. 61532019 and the CDZ project CAP (GZ 1023).

Appendix 0.A Evaluation of Arithmetic Expressions

Below we fix a countable set $\mathcal{X}$ of scalar variables. Given an arithmetic expression $\mathfrak{e}$ over $\mathcal{X}$ and a valuation on $\mathcal{X}$, the element $\mathfrak{e}(\nu)$ is defined inductively on the structure of $\mathfrak{e}$ as follows:

• •

$c(\nu):=c$;

• •

$x(\nu):=\nu(x)$;

• •

${\left\lfloor\frac{\mathfrak{e}}{c}\right\rfloor}(\nu):={\left\lfloor\frac{\mathfrak{e}(\nu)}{c}\right\rfloor}$; (Note that $c\neq 0$ by our assumption.)

• •

${(\mathfrak{e}+\mathfrak{e}^{\prime})}(\nu):=\mathfrak{e}(\nu)+\mathfrak{e}^{\prime}(\nu)$;

• •

${(\mathfrak{e}-\mathfrak{e}^{\prime})}(\nu):=\mathfrak{e}(\nu)-\mathfrak{e}^{\prime}(\nu)$;

• •

${(c*\mathfrak{e}^{\prime})}(\nu):=c\cdot\mathfrak{e}^{\prime}(\nu)$.

Appendix 0.B Semantics of Propositional Arithmetic Predicates

Let $\mathcal{X}$ be the set of scalar variables. The satisfaction relation $\models$ between valuations $\nu$ and propositional arithmetic predicates $\phi$ is defined inductively as follows:

• •

$\nu\models\mathfrak{e}\Join\mathfrak{e}^{\prime}$ ($\Join\in\{\leq,\geq\}$) if $\mathfrak{e}(\nu)\Join\mathfrak{e}^{\prime}(\nu)$;

• •

$\nu\models\neg\phi$ iff $\nu\not\models\phi$;

• •

$\nu\models\phi_{1}\wedge\phi_{2}$ iff $\nu\models\phi_{1}$ and $\nu\models\phi_{2}$;

• •

$\nu\models\phi_{1}\vee\phi_{2}$ iff $\nu\models\phi_{1}$ or $\nu\models\phi_{2}$.

Appendix 0.C Detailed Syntax for Recursive Programs

In the sequel, we fix a countable set of scalar variables; and we also fix a countable set of function names. W.l.o.g, these two sets are pairwise disjoint. Each scalar variable holds an integer upon instantiation.

The Syntax. The syntax of our recursive programs is illustrated by the grammar in Fig. 3. Below we briefly explain the grammar.

• •

Variables: Expressions $\langle\mathit{pvar}\rangle$ range over scalar variables.

• •

Function Names: Expressions $\langle\mathit{fname}\rangle$ range over function names.

• •

Constants: Expressions $\langle\mathit{int}\rangle$ range over integers represented as decimal numbers, while expressions $\langle\mathit{nonzero}\rangle$ range over non-zero integers represented as decimal numbers.

• •

Arithmetic Expressions: Expressions $\langle\mathit{expr}\rangle$ range over linear arithmetic expressions consisting of scalar variables, floor operation (cf. $\left\lfloor\langle\mathit{expr}\rangle/\langle\mathit{nonzero}\rangle\right\rfloor$) and arithmetic operations.

• •

Parameters: Expressions $\langle\mathit{plist}\rangle$ range over lists of scalar variables, and expressions $\langle\mathit{vlist}\rangle$ range over lists of $\langle\mathit{expr}\rangle$ expressions.

• •

Boolean Expressions: Expressions $\langle\mathit{bexpr}\rangle$ range over propositional arithmetic predicates over scalar variables.

• •

Statements: Various types of assignment statements are indicated by ‘$:=$’; ‘skip’ is the statement that does nothing; conditional branch or demonic non-determinism is indicated by the keyword ‘if’, while $\langle\mathit{bexpr}\rangle$ indicates conditional branch and $\star$ indicates demonic non-determinism; while-loops are indicated by the keyword ‘while’; sequential compositions are indicated by semicolon; finally, function calls are indicated by $\langle\mathit{fname}\rangle\left(\langle\mathit{vlist}\rangle\right)$.

• •

Programs: Each recursive program $\langle\mathit{prog}\rangle$ is a sequence of function entities, for which each function entity $\langle\mathit{func}\rangle$ consists of a function name followed by a list of parameters (composing a function declaration) and a curly-braced statement.

Assumptions. W.l.o.g, we consider further syntactical restrictions for simplicity:

• •

Function Entities: we consider that every parameter list $\langle\mathit{plist}\rangle$ contains no duplicate scalar variables, and the function names from function entities are distinct.

• •

Function Calls: we consider that no function call involves some function name without function entity (i.e., undeclared function names).

Appendix 0.D Control-Flow Graphs for Recursive Programs

Intuitive Description. It is intuitively clear that any recursive program can be transformed into a corresponding CFG: one first constructs each ${\rightarrow}_{\mathsf{f}}$ (for $\mathsf{f}\in\mathit{F}$) for each of its function bodies and then groups them together. To construct each ${\rightarrow}_{\mathsf{f}}$, we first construct the partial relation ${\rightarrow}_{P,\mathsf{f}}$ inductively on the structure of $P$ for each statement $P$ appearing in the function body of $\mathsf{f}$, then define ${\rightarrow}_{\mathsf{f}}$ as ${\rightarrow}_{P_{\mathsf{f}},\mathsf{f}}$ for which $P_{\mathsf{f}}$ is the function body of $\mathsf{f}$. Each relation ${\rightarrow}_{P,\mathsf{f}}$ involves two distinguished labels, namely $\ell_{\mathrm{in}}^{P,\mathsf{f}}$ and $\ell_{\mathrm{out}}^{P,\mathsf{f}}$, that intuitively represent the label assigned to the first instruction to be executed in $P$ and the terminal program counter of $P$, respectively; after the inductive construction, $\ell_{\mathrm{in}}^{\mathsf{f}},\ell_{\mathrm{out}}^{\mathsf{f}}$ are defined as $\ell_{\mathrm{in}}^{P_{\mathsf{f}},\mathsf{f}},\ell_{\mathrm{out}}^{P_{\mathsf{f}},\mathsf{f}}$, respectively.

From Programs to CFG’s. In this part, we demonstrate inductively how the control-flow graph of a recursive program can be constructed. Below we fix a recursive program $W$ and denote by $\mathit{F}$ the set of function names appearing in $W$. For each function name $\mathsf{f}\in\mathit{F}$, we define $P_{\mathsf{f}}$ to be the function body of $\mathsf{f}$, and define $V^{\mathsf{f}}$ to be the set of scalar variables appearing in $P_{\mathsf{f}}$ and the parameter list of $\mathsf{f}$.

The control-flow graph of $W$ is constructed by first constructing the counterparts $\{{\rightarrow}_{\mathsf{f}}\}_{\mathsf{f}\in\mathit{F}}$ for each of its function bodies and then grouping them together. To construct each ${\rightarrow}_{\mathsf{f}}$, we first construct the partial relation ${\rightarrow}_{P,\mathsf{f}}$ inductively on the structure of $P$ for each statement $P$ which involves variables solely from $V^{\mathsf{f}}$, then define ${\rightarrow}_{\mathsf{f}}$ as ${\rightarrow}_{P_{\mathsf{f}},\mathsf{f}}$.

Let $\mathsf{f}\in\mathit{F}$. Given an assignment statement of the form ${x}{:=}{\mathfrak{e}}$ involving variables solely from $V^{\mathsf{f}}$ and a valuation $\nu\in\mbox{\sl Val}_{\mathsf{f}}$, we denote by ${\nu}{\left[\mathfrak{e}/x\right]}$ the valuation over $V^{\mathsf{f}}$ such that

[TABLE]

Given a function call $\mathsf{g}(\mathfrak{e}_{1},\dots,\mathfrak{e}_{k})$ with variables solely from $V^{\mathsf{f}}$ and its declaration being $\mathsf{g}(q_{1},\dots,q_{k})$, and a valuation $\nu\in\mbox{\sl Val}_{\mathsf{f}}$, we define ${\nu}{[\mathsf{g},\{\mathfrak{e}_{j}\}_{1\leq j\leq k}]}$ to be a valuation over $V^{\mathsf{g}}$ by:

[TABLE]

Now the inductive construction for each ${\rightarrow}_{P,\mathsf{f}}$ is demonstrated as follows. For each statement $P$ which involves variables solely from $V^{\mathsf{f}}$, the relation ${\rightarrow}_{P,\mathsf{f}}$ involves two distinguished labels, namely $\ell_{\mathrm{in}}^{P,\mathsf{f}}$ and $\ell_{\mathrm{out}}^{P,\mathsf{f}}$, that intuitively represent the label assigned to the first instruction to be executed in $P$ and the terminal program counter of $P$, respectively. After the inductive construction, $\ell_{\mathrm{in}}^{\mathsf{f}},\ell_{\mathrm{out}}^{\mathsf{f}}$ are defined as $\ell_{\mathrm{in}}^{P_{\mathsf{f}},\mathsf{f}},\ell_{\mathrm{out}}^{P_{\mathsf{f}},\mathsf{f}}$, respectively.

Assignments. For $P$ of the form ${x}{:=}{\mathfrak{e}}$ or skip, ${\rightarrow}_{P,\mathsf{f}}$ involves a new assignment label $\ell_{\mathrm{in}}^{P,\mathsf{f}}$ (as the initial label) and a new branching label $\ell_{\mathrm{out}}^{P,\mathsf{f}}$ (as the terminal label), and contains a sole triple $\left(\ell_{\mathrm{in}}^{P,\mathsf{f}},\nu\mapsto{\nu}{\left[\mathfrak{e}/x\right]},\ell_{\mathrm{out}}^{P,\mathsf{f}}\right)$ or $\left(\ell_{\mathrm{in}}^{P,\mathsf{f}},\nu\mapsto\nu,\ell_{\mathrm{out}}^{P,\mathsf{f}}\right)$, respectively. 2. 2.

Function Calls. For $P$ of the form $\mathsf{g}(\mathfrak{e}_{1},\dots,\mathfrak{e}_{k})$, ${\rightarrow}_{P,\mathsf{f}}$ involves a new call label $\ell_{\mathrm{in}}^{P,\mathsf{f}}$ and a new branching label $\ell_{\mathrm{out}}^{P,\mathsf{f}}$, and contains a sole triple $\left(\ell_{\mathrm{in}}^{P,\mathsf{f}},\left(\mathsf{g},\nu\mapsto\nu[\mathsf{g},\{\mathfrak{e}_{j}\}_{1\leq j\leq k}]\right),\ell_{\mathrm{out}}^{P,\mathsf{f}}\right)$. 3. 3.

Sequential Statements. For ${P}{=}{Q_{1};Q_{2}}$, we take the disjoint union of ${\rightarrow}_{Q_{1},\mathsf{f}}$ and ${\rightarrow}_{Q_{2},\mathsf{f}}$, while redefining $\ell_{\mathrm{out}}^{Q_{1},\mathsf{f}}$ to be $\ell_{\mathrm{in}}^{Q_{2},\mathsf{f}}$ and putting $\ell_{\mathrm{in}}^{P,\mathsf{f}}:=\ell_{\mathrm{in}}^{Q_{1},\mathsf{f}}$ and $\ell_{\mathrm{out}}^{P,\mathsf{f}}:=\ell_{\mathrm{out}}^{Q_{2},\mathsf{f}}$. 4. 4.

If-Branches. For {P}{=}{\textbf{if \phi then }Q_{1}\textbf{ else }Q_{2}\textbf{ fi}} with $\phi$ being a propositional arithmetic predicate, we first add two new branching labels $\ell_{\mathrm{in}}^{P},\ell_{\mathrm{out}}^{P}$, then take the disjoint union of ${\rightarrow}_{Q_{1},\mathsf{f}}$ and ${\rightarrow}_{Q_{2},\mathsf{f}}$ while simultaneously identifying both $\ell_{\mathrm{out}}^{Q_{1},\mathsf{f}}$ and $\ell_{\mathrm{out}}^{Q_{2},\mathsf{f}}$ with $\ell_{\mathrm{out}}^{P,\mathsf{f}}$, and finally obtain ${\rightarrow}_{P,\mathsf{f}}$ by adding two triples $(\ell_{\mathrm{in}}^{P,\mathsf{f}},\phi,\ell_{\mathrm{in}}^{Q_{1},\mathsf{f}})$ and $(\ell_{\mathrm{in}}^{P,\mathsf{f}},\neg\phi,\ell_{\mathrm{in}}^{Q_{2},\mathsf{f}})$ into the disjoint union of ${\rightarrow}_{Q_{1},\mathsf{f}}$ and ${\rightarrow}_{Q_{2},\mathsf{f}}$. 5. 5.

While-Loops. For ${P}{=}{\mbox{ {while} }\phi\mbox{ {do} }Q\mbox{ {od}}}$, we add a new branching label $\ell_{\mathrm{out}}^{P,\mathsf{f}}$ as a terminal label and obtain ${\rightarrow}_{P,\mathsf{f}}$ by adding triples $(\ell_{\mathrm{out}}^{Q,\mathsf{f}},\phi,\ell_{\mathrm{in}}^{Q,\mathsf{f}})$ and $(\ell_{\mathrm{out}}^{Q,\mathsf{f}},\neg\phi,\ell_{\mathrm{out}}^{P,\mathsf{f}})$ into ${\rightarrow}_{Q,\mathsf{f}}$, and define $\ell_{\mathrm{in}}^{P,\mathsf{f}}:=\ell_{\mathrm{out}}^{Q,\mathsf{f}}$. 6. 6.

Demonic Nondeterminism. For {P}{=}{\textbf{if \star then }Q_{1}\textbf{ else }Q_{2}\textbf{ fi}}, we first add a new demonic label $\ell_{\mathrm{in}}^{P}$ and a new branching labels $\ell_{\mathrm{out}}^{P}$, then take the disjoint union of ${\rightarrow}_{Q_{1},\mathsf{f}}$ and ${\rightarrow}_{Q_{2},\mathsf{f}}$ while simultaneously identifying both $\ell_{\mathrm{out}}^{Q_{1},\mathsf{f}}$ and $\ell_{\mathrm{out}}^{Q_{2},\mathsf{f}}$ with $\ell_{\mathrm{out}}^{P,\mathsf{f}}$, and finally obtain ${\rightarrow}_{P,\mathsf{f}}$ by adding two triples $(\ell_{\mathrm{in}}^{P,\mathsf{f}},\star,\ell_{\mathrm{in}}^{Q_{1},\mathsf{f}})$ and $(\ell_{\mathrm{in}}^{P,\mathsf{f}},\star,\ell_{\mathrm{in}}^{Q_{2},\mathsf{f}})$ into the disjoint union of ${\rightarrow}_{Q_{1},\mathsf{f}}$ and ${\rightarrow}_{Q_{2},\mathsf{f}}$.

Appendix 0.E Definition for Reachability

Definition 7 (Reachability)

Let $\mathsf{f}^{*}$ be a function name and $\phi^{*}$ be a propositional arithmetic predicate over $V^{\mathsf{f^{*}}}$. A configuration $w$ is reachable w.r.t $\mathsf{f}^{*},\phi^{*}$ if there exist a scheduler $\pi$ and a stack element $(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)$ such that (i) $\nu\models\phi^{*}$ and (ii) $w$ appears in the run $\rho((\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu),\pi)$. A stack element $\mathfrak{c}$ is reachable w.r.t $\mathsf{f}^{*},\phi^{*}$ if there exists a configuration $w$ reachable w.r.t $\mathsf{f}^{*},\phi^{*}$ such that $w=\mathfrak{c}\cdot w^{\prime}$ for some configuration $w^{\prime}$.

Appendix 0.F Proof for Theorem 3.1: Soundness

Theorem 3.1. (Soundness). For all measure functions $g$ w.r.t $\mathsf{f}^{*},\phi^{*}$, it holds that for all valuations $\nu\in\mbox{\sl Val}_{\mathsf{\mathsf{f}^{*}}}$ such that $\nu\models\phi^{*}$, we have $\overline{T}(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)\leq g(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)$.

Proof

Define the function $h$ from the set of configurations into $[0,\infty]$ as follows:

[TABLE]

where $h(\varepsilon):=0$. We show that $h$ can be deemed as a ranking function over the set of reachable configurations w.r.t $\mathsf{f}^{*},\phi^{*}$.

Let $\nu\in\mbox{\sl Val}_{\mathsf{f^{*}}}$ be any valuation such that $\nu\models\phi^{*}$ and $\pi$ be any scheduler for $P$. Moreover, let $\rho\left((\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu),\pi\right)=\{w_{n}\}_{n\in\mathbb{N}_{0}}$. Since the case $g(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)=\infty$ is trivial, we only consider the case $g(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)<\infty$.

By Definition 7, every $w_{n}$ is reachable w.r.t $\mathsf{f}^{*},\phi^{*}$. Hence, by Definition 4, (a) for all $n\in\mathbb{N}_{0}$, if $w_{n}\neq\varepsilon$ then $h(w_{n})\geq 1$, and $h(w_{n})=0$ otherwise. Furthermore, by Definition 4 and our semantics,one can easily verify that (b) for all $n\in\mathbb{N}_{0}$ , if $w_{n}\neq\varepsilon$ then $h(w_{n+1})\leq h(w_{n})-1$.

To see (b), consider for example the function-call case where $w_{n}=(\mathsf{f},\ell,\nu)\cdot w^{\prime}$, $\ell\in\mathit{L}_{\mathrm{c}}^{\mathsf{f}}$ and $(\ell,(\mathsf{g},f),\ell^{\prime})$ is the only triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. Then by our semantics, $h(w_{n})=g(\mathsf{f},\ell,\nu)+h(w^{\prime})$ and $h(w_{n+1})=g(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},f(\nu))+g(\mathsf{f},\ell^{\prime},\nu)+h(w^{\prime})$. Thus by C3, $h(w_{n+1})+1\leq h(w_{n})$. The other cases (namely assignment, branching and nondeterminism) can be verified similarly through a direct investigation of our semantics and an application of C2, C4 or C5.

From (a), (b) and the fact that $h(w_{0})=g(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)<\infty$, one has that $m:=T\left((\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu),\pi\right)<\infty$ (or otherwise (a) and (b) cannot hold simultaneously). Furthermore, from an easy inductive proof based on (b), one has that $h(w_{m})\leq h(w_{0})-m$. Together with $h(w_{m})=0$ (from (a)), one obtains that

[TABLE]

Hence, $\overline{T}(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)\leq g(\mathsf{f}^{*},\ell_{\mathrm{in}}^{\mathsf{f}^{*}},\nu)$ .∎

Appendix 0.G Proof for Theorem 3.1: Completeness

We recall that for each $\mathsf{f}\in\mathit{F}$ and $\ell\in\mathit{L}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, we define $D_{\mathsf{f},\ell}$ to be the set of all valuations $\nu$ w.r.t $\mathsf{f}$ such that $(\mathsf{f},\ell,\nu)$ is reachable w.r.t $\mathsf{f}^{*},\phi^{*}$.

We introduce some notations for schedulers. Let $\pi$ be a scheduler for $P$ and $\mathfrak{c}$ be a non-terminal stack element. We define $\mathrm{post}(\pi,\mathfrak{c})$ to be the scheduler such that for any non-empty finite word of configurations $w_{0}\dots w_{n}$ with $w_{n}$ being non-deterministic,

[TABLE]

In the case that $\mathfrak{c}$ is not non-deterministic, we define $\mathrm{pre}(\pi,\mathfrak{c})$ to be one of the schedulers such that for any non-empty finite word of configurations $w_{0}\dots w_{n}$ with $w_{n}$ being non-deterministic,

[TABLE]

the decisions of $\mathrm{pre}(\pi,\mathfrak{c})$ at finite words not starting with $\mathfrak{c}$ will be irrelevant. In the case that $\mathfrak{c}=(\mathsf{f},\ell,\nu)$ is non-deterministic, for any given $\ell^{\prime}\in\mathit{L}^{\mathsf{f}}$ such that $(\ell,\star,\ell^{\prime})\in{\rightarrow}_{\mathsf{f}}$, we define $\mathrm{pre}(\pi,(\mathfrak{c},\ell^{\prime}))$ to be one of the schedulers such that (i)

[TABLE]

and (ii) for any non-empty finite word of configurations $w_{0}\dots w_{n}$ with $w_{n}$ being non-deterministic,

[TABLE]

again, the decisions of $\mathrm{pre}(\pi,(\mathfrak{c},\ell^{\prime}))$ at finite words not starting with $\mathfrak{c}$ will be irrelevant.

Theorem 3.1. (Completeness). $\overline{T}$ is a measure function w.r.t $\mathsf{f}^{*},\phi^{*}$.

Proof

We prove that $\overline{T}$ satisfies the conditions C1–C5 in Definition 4 with equality. Condition C1 follows directly from the definition. Below we prove that C2–C5 hold.

Let $\mathfrak{c}=(\mathsf{f},\ell,\nu)$ be a non-terminal stack element such that $\nu\in D_{\mathsf{f},\ell}$. Below we clarify several cases on $\mathfrak{c}$.

Case 1 (cf. C2):

$\ell\in\mathit{L}_{\mathrm{a}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$ and $(\ell,f,\ell^{\prime})$ is the only triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. Consider any scheduler $\pi$ for $W$. By our semantics, one can prove easily that

• •

$T\left((\mathsf{f},\ell,\nu),\pi\right)=1+T\left(\left(\mathsf{f},\ell^{\prime},f(\nu)\right),\mathrm{post}(\pi,\mathfrak{c})\right)$, and

• •

$T\left((\mathsf{f},\ell,\nu),\mathrm{pre}(\pi,\mathfrak{c})\right)=1+T\left(\left(\mathsf{f},\ell^{\prime},f(\nu)\right),\pi\right)$.

Since $\pi$ is arbitrarily, by taking the supremum at the both sides of the equalities above one has that

[TABLE]

Case 2 (cf. C3):

$\ell\in\mathit{L}_{\mathrm{c}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$ and $(\ell,(\mathsf{g},f),\ell^{\prime})$ is the only triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$.

We first consider the case $\overline{T}(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu)=\infty$, meaning that schedulers $\pi$ can make $T\left((\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu),\pi\right)$ arbitrarily large. Since for any scheduler $\pi$, $T\left((\mathsf{f},\ell,\nu),\mathrm{pre}(\pi,\mathfrak{c})\right)\geq 1+T\left((\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu),\pi\right)$, one has that

[TABLE]

Then we consider the case that $\overline{T}(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu)<\infty$. On one hand, let $\pi$ be any scheduler for $W$. Since $T\left((\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu),\mathrm{post}(\pi,\mathfrak{c})\right)<\infty$, one can find a (unique) finite prefix $\gamma$ of the run $\rho\left((\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu),\mathrm{post}(\pi,\mathfrak{c})\right)$ consisting of only non-empty (i.e. not $\varepsilon$) configurations which describes the finite execution of the function call $\mathsf{g}$ under the scheduler $\mathrm{post}(\pi,\mathfrak{c})$. By our semantics, one can prove easily that

[TABLE]

where $\pi^{\prime}$ is the scheduler such that for any non-empty finite word of configurations $w_{0}\dots w_{n}$ with $w_{n}$ being non-deterministic, $\pi^{\prime}(w_{0}\dots w_{n})=\pi(\mathfrak{c}\cdot\gamma\cdot w_{0}\dots w_{n})$. It follows from the arbitrary choice of $\pi$ that

[TABLE]

On the other hand, let $\pi_{1},\pi_{2}$ be any two schedulers for $P$. Since $\overline{T}\left(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu\right)<\infty$, one can find a (unique) finite prefix $\gamma$ of the run $\rho\left((\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},\nu),\pi_{1}\right)$ consisting of only non-empty (i.e. not $\varepsilon$) configurations which describes the finite execution of the function call $\mathsf{g}$ under the scheduler $\pi_{1}$. Then

[TABLE]

where $\pi$ is one of the schedulers such that (i) $\pi(\mathfrak{c}\cdot\beta)=\pi_{1}(\beta)$ whenever $\beta$ ends at a non-deterministic configuration and is a prefix of $\gamma$ (including $\gamma$) and (ii) $\pi(\mathfrak{c}\cdot\gamma\cdot\beta)=\pi_{2}(\beta)$ whenever $\beta$ is non-empty and ends at a non-deterministic configuration. Thus, by the arbitrary choice of $\pi_{1},\pi_{2}$, one has that

[TABLE]

In either case, we have

[TABLE]

Case 3 (cf. C4):

$\ell\in\mathit{L}_{\mathrm{b}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$ and $(\ell,\phi,\ell_{1}),(\ell,\neg\phi,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. By our semantics, one can easily prove that

[TABLE]

for any scheduler $\pi$ for $W$, and

[TABLE]

for any schedulers $\pi_{1},\pi_{2}$ for $P$, where $\pi$ is either $\mathrm{pre}\left(\pi_{1},\mathfrak{c}\right)$ if $\nu\models\phi$, or $\mathrm{pre}\left(\pi_{2},\mathfrak{c}\right)$ if $\nu\models\neg\phi$. By taking the supremum at the both sides of the equalities above, one has

[TABLE]

Case 4 (cf. C5):

$\ell\in\mathit{L}_{\mathrm{d}}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$ and $(\ell,\star,\ell_{1}),(\ell,\star,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. By our semantics, one easily proves that

[TABLE]

for any scheduler $\pi$ (for $P$), and

[TABLE]

for any schedulers $\pi,\pi_{1},\pi_{2}$ such that $\pi$ is either $\mathrm{pre}(\pi_{1},(\mathfrak{c},\ell_{1}))$ if $T\left((\mathsf{f},\ell_{1},\nu),\pi_{1}\right)\geq T\left((\mathsf{f},\ell_{2},\nu),\pi_{2}\right)$, or $\mathrm{pre}(\pi_{2},(\mathfrak{c},\ell_{2}))$ if otherwise. By taking the supremum at the both sides of the equalities above, one obtains

[TABLE]

∎

Appendix 0.H Omitted Details in Significant Label Construction

Expansion Construction (from $g$ to $\widehat{g}$)

In the following, we illustrate how one can obtain a measure function from a function defined only on significant labels. Let $g$ be a function from $\left\{(\mathsf{f},\ell,\nu)\mid\mathsf{f}\in\mathit{F},\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}},\nu\in\mbox{\sl Val}_{\mathsf{f}}\right\}$ into $[0,\infty]$. The function expanded from $g$, denoted by $\widehat{g}$, is a function from the set of all stack elements into $[0,\infty]$ inductively defined through the procedure described as follows.

Initial Step. If $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$, then $\widehat{g}(\mathsf{f},\ell,\nu):=g(\mathsf{f},\ell,\nu)$ . 2. 2.

Termination. If $\ell=\ell_{\mathrm{out}}^{\mathsf{f}}$, then $\widehat{g}(\mathsf{f},\ell,\nu):=0$ . 3. 3.

Assignment. If $\ell\in\mathit{L}_{\mathrm{a}}^{\mathsf{f}}\backslash\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ with $(\ell,h,\ell^{\prime})$ being the only triple in ${\rightarrow}_{\mathsf{f}}$ and $\widehat{g}(\mathsf{f},\ell^{\prime},\centerdot)$ is already defined, then $\widehat{g}(\mathsf{f},\ell,\nu):=1+\widehat{g}(\mathsf{f},\ell^{\prime},h(\nu))$. 4. 4.

Branching. If $\ell\in\mathit{L}_{\mathrm{b}}^{\mathsf{f}}\backslash\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ with $(\ell,\phi,\ell_{1})$, $(\ell,\neg\phi,\ell_{2})$ being namely the two triples in ${\rightarrow}_{\mathsf{f}}$ and both $\widehat{g}(\mathsf{f},\ell_{1},\centerdot)$ and $\widehat{g}(\mathsf{f},\ell_{2},\centerdot)$ is already defined, then $\widehat{g}(\mathsf{f},\ell,\nu):=\mathbf{1}_{\nu\models\phi}\cdot\widehat{g}(\mathsf{f},\ell_{1},\nu)+\mathbf{1}_{\nu\models\neg\phi}\cdot\widehat{g}(\mathsf{f},\ell_{2},\nu)+1$; 5. 5.

Call. If $\ell\in\mathit{L}_{\mathrm{c}}^{\mathsf{f}}\backslash\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ with $(\ell,(\mathsf{g},h),\ell^{\prime})$ being the only triple in ${\rightarrow}_{\mathsf{f}}$ and $\widehat{g}(\mathsf{f},\ell^{\prime},\centerdot)$ is already defined, then $\widehat{g}(\mathsf{f},\ell,\nu):=g(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},h(\nu))+\widehat{g}(\mathsf{f},\ell^{\prime},\nu)+1$. 6. 6.

Non-determinism. If $\ell\in\mathit{L}_{\mathrm{d}}^{\mathsf{f}}\backslash\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ with $(\ell,\star,\ell_{1})$, $(\ell,\star,\ell_{2})$ being namely the two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$ and both $\widehat{g}(\mathsf{f},\ell_{1},\centerdot)$ and $\widehat{g}(\mathsf{f},\ell_{2},\centerdot)$ is already defined, then $\widehat{g}(\mathsf{f},\ell,\nu):=\max\left\{\widehat{g}(\mathsf{f},\ell_{1},\nu),\widehat{g}(\mathsf{f},\ell_{2},\nu)\right\}+1$.

Note that in the previous expansion construction, we have not technically shown that $\widehat{g}$ is defined over all stack elements. The following technical lemma shows that the function $\widehat{g}$ is indeed well-defined.

Lemma 1

For each function $g$ from $\left\{(\mathsf{f},\ell,\nu)\mid\mathsf{f}\in\mathit{F},\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}},\nu\in\mbox{\sl Val}_{\mathsf{f}}\right\}$ into $[0,\infty]$, the function $\widehat{g}$ is well-defined.

Proof

Suppose that $\widehat{g}$ is not well-defined, i.e., there exists some $\mathsf{f}\in\mathit{F}$ and $\ell_{0}\in\mathit{L}^{\mathsf{f}}$ such that $\widehat{g}(\mathsf{f},\ell_{0},\centerdot)$ remains undefined. Then by the inductive procedure, there exists a triple $(\ell_{0},\alpha,\ell_{1})$ in ${\rightarrow}_{\mathsf{f}}$ such that $\widehat{g}(\mathsf{f},\ell_{1},\centerdot)$ remains undefined. With the same reasoning, one can inductively construct an infinite sequence $\{\ell_{j}\}_{j\in\mathbb{N}_{0}}$ such that each $\widehat{g}(\mathsf{f},\ell_{j},\centerdot)$ remains undefined. Since $\mathit{L}^{\mathsf{f}}$ is finite, there exist $j_{1},j_{2}$ such that $j_{1}\neq j_{2}$ and $\ell_{j_{1}}=\ell_{j_{2}}$. It follows from our semantics that there exists $j^{*}$ such that $j_{1}\leq j^{*}\leq j_{2}$ and $\ell_{j^{*}}$ corresponds to the initial label of a while-loop in $W$. Contradiction to the fact that $\ell_{j^{*}}\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$.∎

Proposition 2

Let $g$ be a function from $\left\{(\mathsf{f},\ell,\nu)\mid\mathsf{f}\in\mathit{F},\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}},\nu\in\mbox{\sl Val}_{\mathsf{f}}\right\}$ into $[0,\infty]$. Let $I$ be an invariant w.r.t $\mathsf{f}^{*},\phi^{*}$. Consider that for all stack elements $(\mathsf{f},\ell,\nu)$ such that $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ and $\nu\models I(\mathsf{f},\ell)$, the following conditions hold:

• •

C2’:* if $\ell\in\mathit{L}_{\mathrm{a}}^{\mathsf{f}}$ and $(\ell,f,\ell^{\prime})$ is the only triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$, then $\widehat{g}(\mathsf{f},\ell^{\prime},f(\nu))+1\leq\widehat{g}(\mathsf{f},\ell,\nu)$;*

• •

C3’:* if $\ell\in\mathit{L}_{\mathrm{c}}^{\mathsf{f}}$ and $(\ell,(\mathsf{g},f),\ell^{\prime})$ is the only triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$, then $1+\widehat{g}(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},f(\nu))+\widehat{g}(\mathsf{f},\ell^{\prime},\nu)\leq\widehat{g}(\mathsf{f},\ell,\nu)$;*

• •

C4’:* if $\ell\in\mathit{L}_{\mathrm{b}}^{\mathsf{f}}$ and $(\ell,\phi,\ell_{1}),(\ell,\neg\phi,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$, then $\mathbf{1}_{\nu\models\phi}\cdot\widehat{g}(\mathsf{f},\ell_{1},\nu)+\mathbf{1}_{\nu\models\neg\phi}\cdot\widehat{g}(\mathsf{f},\ell_{2},\nu)+1\leq\widehat{g}(\mathsf{f},\ell,\nu)$ ;*

• •

C5’:* if $\ell\in\mathit{L}_{\mathrm{d}}^{\mathsf{f}}$ and $(\ell,\star,\ell_{1}),(\ell,\star,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$, then $\max\{\widehat{g}(\mathsf{f},\ell_{1},\nu),\widehat{g}(\mathsf{f},\ell_{2},\nu)\}+1\leq\widehat{g}(\mathsf{f},\ell,\nu)$.*

Then $\widehat{g}$ is a measure function w.r.t $\mathsf{f}^{*},\phi^{*}$.

Proof

The proof follows directly from the fact that (i) all valuations in $D_{\mathsf{f},\ell}$ satisfy $I(\mathsf{f},\ell)$, for all $\mathsf{f}\in\mathit{F}$ and $\ell\in\mathit{L}^{\mathsf{f}}\backslash\{\ell_{\mathrm{out}}^{\mathsf{f}}\}$, (ii) C2’-C5’ directly implies C2-C5 for $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ and (iii) C1-C5 are automatically satisfied for $\ell\not\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}$ by the expansion construction of significant labels. ∎

Appendix 0.I Omitted Details for Sect. 4

In this section, we present the omitted details on our algorithm for synthesizing measure functions. As mentioned before, the synthesis algorithm is designed to synthesize one function over valuations at each function name and appropriate significant label, so that conditions C2’-C5’ in Proposition 2 are fulfilled.

Below we fix an input recursive program $P$ with its CFG taking the form (${\dagger}$), an input invariant $I$ in disjunctive normal form and an input pair of parameters $(d,\mathrm{op},r,k)$. We demonstrate our algorithm step in step as follows.

0.I.1 Step 1 of SynAlgo

All details are presented in the main article.

0.I.2 Step 2 of SynAlgo

Computation of $\widehat{\llbracket\eta\rrbracket}$

In the computation, we use the fact that for real-valued functions $\{f_{i}\}_{1\leq i\leq m}$, $\{g_{j}\}_{1\leq j\leq n}$ and $h$, it holds that

[TABLE]

and

[TABLE]

provided that $h$ is everywhere non-negative, where the maximum function over a finite set of functions is defined in pointwise fashion. Moreover, we use the facts that (i)

[TABLE]

for all propositional arithmetic predicates $\phi_{1},\phi_{2}$ and valuations $\nu$, and (ii)

[TABLE]

provided that (a) $\bigvee_{i}\phi_{i},\bigvee_{j}\psi_{j}$ are both tautology and (b) $\phi_{i_{1}}\wedge\phi_{i_{2}},\psi_{j_{1}}\wedge\psi_{j_{2}}$ are both unsatisfiable whenever $i_{1}\neq i_{2}$ and $j_{1}\neq j_{2}$, and (iii) propositional arithmetic predicates are closed under substitution of expressions in $\langle\mathit{expr}\rangle$ for scalar variables.

0.I.3 Step 3 of SynAlgo

Establishment of Constraint Triples.

Based on $\widehat{\llbracket\eta\rrbracket}$, the algorithm generates constraint triples at each significant label, then group all generated constraint triples together in a conjunctive way.

Let $\ell$ be any significant label at any function name $\mathsf{f}$, the algorithm generates constraint triples at $\mathsf{f},\ell$ as follows. W.l.o.g, let $I(\mathsf{f},\ell)=\bigvee_{l}\Psi_{l}$ where each $\Psi_{l}$ is a conjunction of atomic formulae of the form $\mathfrak{e}\geq 0$. The algorithm first generate constraint triples related to non-negativity of measure functions.

• •

Non-negativity: The algorithm generates the collection of constraint triples

[TABLE]

Then the algorithm generates constraint triples through C2’-C5’ as follows.

• •

Case 1 (C2’): $\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}}\cap\mathit{L}_{\mathrm{a}}^{\mathsf{f}}$ and $(\ell,f,\ell^{\prime})$ is the sole triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. As $\widehat{\llbracket\eta\rrbracket}(\mathsf{f},\ell^{\prime},\centerdot)$ can be represented in the form (2), $\widehat{\llbracket\eta\rrbracket}(\mathsf{f},\ell^{\prime},f(\centerdot))$ can also be represented by an expression

[TABLE]

in the form (2). Let a disjunctive normal form of each formula $I(\mathsf{f},\ell)\wedge\phi_{ij}$ be $\bigvee_{l}\Phi_{ij}^{l}$, where each $\Phi_{ij}^{l}$ is a conjunction of atomic formulae of the form $\mathfrak{e}^{\prime}\geq 0$. Then the algorithm generates the collection of constraint triples

[TABLE]

• •

Case 2 (C3’): $\ell\in\mathit{L}_{\mathrm{c}}^{\mathsf{f}}$ and $(\ell,(\mathsf{g},f),\ell^{\prime})$ is the sole triple in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. Let $\widehat{\llbracket\eta\rrbracket}\left(\mathsf{g},\ell_{\mathrm{in}}^{\mathsf{g}},f(\centerdot)\right)+\widehat{\llbracket\eta\rrbracket}(\mathsf{f},\ell^{\prime},\centerdot)$ be represented by the expression

[TABLE]

in the form (2). Let a disjunctive normal form of each formula $I(\mathsf{f},\ell)\wedge\phi_{ij}$ be $\bigvee_{l}\Phi_{ij}^{l}$, where each $\Phi_{ij}^{l}$ is a conjunction of atomic formulae of the form $\mathfrak{e}^{\prime}\geq 0$. Then the algorithm generates the collection of constraint triples

[TABLE]

• •

Case 3 (C4’): $\ell\in\mathit{L}_{\mathrm{b}}^{\mathsf{f}}$ and $(\ell,\phi,\ell_{1}),(\ell,\neg\phi,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. Let $h$ be the function (parametric on template variables)

[TABLE]

Then $h$ can be represented by an expression

[TABLE]

in the form (2). Let a disjunctive normal form of each formula $I(\mathsf{f},\ell)\wedge\phi_{ij}$ be $\bigvee_{l}\Phi_{ij}^{l}$, where each $\Phi_{ij}^{l}$ is a conjunction of atomic formulae of the form $\mathfrak{e}^{\prime}\geq 0$. Then the algorithm generates the collection of constraint triples

[TABLE]

• •

Case 4 (C5’) $\ell\in\mathit{L}_{\mathrm{d}}^{\mathsf{f}}$ and $(\ell,\star,\ell_{1}),(\ell,\star,\ell_{2})$ are namely two triples in ${\rightarrow}_{\mathsf{f}}$ with source label $\ell$. Let $h$ be the function (parametric on template variables)

[TABLE]

otherwise. Then $h$ can be represented by an expression

[TABLE]

in the form (2). Let a disjunctive normal form of each formula $I(\mathsf{f},\ell)\wedge\phi_{ij}$ be $\bigvee_{l}\Phi_{ij}^{l}$. Then the algorithm generates the collection of constraint triples

[TABLE]

After generating the constraint triples for each significant label, the algorithm group them together in the conjunctive fashion to form a single collection of constraint triples.

0.I.4 Step 4 of SynAlgo

All details of Step 4 is in the main text.

0.I.5 Step 5 of SynAlgo

All details are presented in the main article.

Theorem 4.4. Our algorithm, SynAlgo, is a sound approach for the RecTermBou problem, i.e., if SynAlgo succeeds to synthesize a function $g$ on $\left\{(\mathsf{f},\ell,\nu)\mid\mathsf{f}\in\mathit{F},\ell\in\mathit{L}_{\mathrm{s}}^{\mathsf{f}},\nu\in\mbox{\sl Val}_{\mathsf{f}}\right\}$, then $\widehat{g}$ is a measure function and hence an upper bound on the pessimistic termination time.

Proof

The proof follows from the facts that (i) once the logical formulae encoded by the constraint triples (cf. semantics of constraint triples specified in Step 3) are fulfilled by template variables, then $\widehat{\llbracket\eta\rrbracket}$ (obtained in Step 2, with $\eta$ being the template established in Step 1) satisfies the conditions specified in Proposition 2, (ii) the variable abstraction (i.e., the linear inequalities) in Step 4 is a sound over-approximation for floored expressions, logarithmic terms and exponentiation terms, and (iii) Handelman’s Theorem provides a sound form for positive polynomials over polyhedra.∎

Appendix 0.J Illustration on Merge-Sort

We now present a step-by-step illustration of our entire method (from syntax, to semantics, to all the steps of the algorithm) on the classical Merge-Sort. This illustrates the quite involved aspects of our approach.

0.J.1 Program Implementation

Figure 4 represents an implementation for the Merge-Sort algorithm [23, Chapter 2] in our language. The numbers on the leftmost side are the labels assigned to statements which represent program counters, where the function $\mathsf{mergesort}$ starts from label $1$ and ends at $7$, and $\mathsf{merge}$ starts from label $8$ and ends at $22$.

In detail, the scalar variable $i$ (resp. $j$) in both the parameter list of $\mathsf{mergesort}$ and that of $\mathsf{merge}$ represents the start (resp. the end) of the array index; the scalar variable $k$ in the parameter list of $\mathsf{merge}$ represents the separating index for merging two sub-arrays between $i,j$; moreover, in $\mathsf{merge}$, the demonic nondeterministic branch (at program counter $12$) abstracts the comparison between array entries and the skip’s at program counters $13,15,20$ represent corresponding array assignment statements in a real implementation for Merge-Sort.

The replacement of array-relevant operations with either skip or demonic non-determinism preserves worst-case complexity as demonic non-determinism over-approximates conditional branches involving array entries.

0.J.2 Control Flow Graph and Significant Labels

To begin the analysis, the algorithm must first obtain the control-flow graph (CFG) of the program. This is depicted in Figures 7,  7 and  7.

For brevity we define $\phi:=1\leq i\wedge i\leq j-1$, $\psi:=l\leq j$, and let id indicate the identity function. The update functions ($f_{i}$’s and $g_{i}$’s) are given in Figure 7. Moreover, in Figure 7, any $\overline{q}$ is the concrete entity held by the scalar variable $q$ under the valuation at runtime, and every function is represented in the form “$p\leftarrow q$” meaning “$q$ assigned to $p$”, where only the relevant variable is shown for assignment functions.

Figure 7 shows that $\mathsf{mergesort}$ (cf. Fig. 4) starts from the if-branch with guard $\phi$ (label $1$). Then if $\phi$ is satisfied (i.e., the length of the array is greater than one), the program steps into the recursive step which is composed of labels 2–5; otherwise, the program proceeds to terminal label $7$ through $6$ with nothing done.

Figure 7 shows that $\mathsf{merge}$ (cf. Fig. 4) starts from a series of assignments (labels 8–10) and then enters the while-loop (labels 11–17) which does the merging of two sub-arrays; after the while-loop starting from $11$, the program enters the part for copying array-content back (labels 18–21) and finally enters the terminal label $22$.

The types of labels are straightforward. In $\mathsf{mergesort}$, labels $2,6$ are assignment labels, label $1$ is a branching label, labels $3\mbox{--}5$ are call labels. In $\mathsf{merge}$, labels $8\mbox{--}10,13\mbox{--}18,20\mbox{--}21$ are assignment labels, labels $11,19$ are branching labels, and label $12$ is a demonic non-deterministic point.

In this program, significant labels are $1$ and $8$ (beginning points of functions) and $11$ and $19$ (while loop headers).

0.J.3 Step 1: Invariants and Templates

As mentioned in Section 3, automatic obtaining of invariants is a standard problem with several known techniques[25, 18]. Since invariant generation is not a main part of our algorithm, we simply use the straightforward invariants in Table 2 to demonstrate our algorithm.

The algorithm constructs a template $\eta(\mathsf{f},\ell,\centerdot)$ of the form shown in (1) at every significant label. Due to the large amount of space needed to illustrate the method on the complete template, for the sake of this example, we restrict our templates to the forms presented in Table 3 instead. Since a template with this restricted form is feasible, the whole template consisting of all products of pairs of terms is also feasible. Here the $c_{i}$’s are variables that the algorithm needs to synthesize.

Note that the results reported in Section 5 were obtained by our implementation in the general case, where the templates were not given as part of input and were generated automatically by our algorithm in their full form according to (1).

0.J.4 Step 2: Computation of $\widehat{\llbracket\eta\rrbracket}$

In this step, the algorithm expands the $\eta$ generated for significant labels in the previous step to obtain $\widehat{\llbracket\eta\rrbracket}$ for all labels. This results in a function of form (2). In order to make equations easier to read, we use the notation $\binom{\phi}{p}$ to denote $\mathbf{1}_{\phi}\cdot p$ in this section. We also use $\widehat{\llbracket\eta\rrbracket}(\mathsf{f},\ell)[p\leftarrow\mathfrak{e}]$ to denote the result of replacing every occurrence of the variable $p$ in $\widehat{\llbracket\eta\rrbracket}(\mathsf{f},\ell)$ with the expression $\mathfrak{e}$.

End points of functions. The algorithm sets $\widehat{\llbracket\eta\rrbracket}(\mathsf{mergesort},7)$ and $\widehat{\llbracket\eta\rrbracket}(\mathsf{merge},22)$ to [math], since these correspond to the terminal labels of their respective functions.

Significant Labels. For each significant label $\ell$ of a function $\mathsf{f}$, the algorithm, by definition, sets $\widehat{\llbracket\eta\rrbracket}(\mathsf{f},\ell)$ to:

[TABLE]

Therefore we have:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Expansion to Other Labels. By applying C1-C5 the algorithm calculates $\widehat{\llbracket\eta\rrbracket}$ for all labels in the following order:

[TABLE]

The concrete values of $\widehat{\llbracket\eta\rrbracket}$’s calculated as above are too long to present in the paper. Therefore we only include some of them to illustrate the method:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

The algorithm utilizes Farkas lemma to simplify the $\widehat{\llbracket\eta\rrbracket}$’s and remove unnecessary terms. Hence, at the end of this step we will have:

[TABLE]

0.J.5 Step 3: Establishment of Constraint Triples

A constraint triple $(\mathsf{f},\phi,\mathfrak{e})$ denotes $\forall\nu\in\mbox{\sl Val}_{\mathsf{f}}.\left(\nu\models\phi\rightarrow\llbracket\mathfrak{e}\rrbracket(\nu)\geq 0\right)$ , i.e., each triple consists of a function name, a precondition $\phi$ and an expression $\mathfrak{e}$. This means that the unknown variables ($c_{i}$ ’s) should be assigned values in a way that whenever $\phi$ is satisfied, we have $\mathfrak{e}\geq 0$. When several triples are obtained, we group them together in a conjunctive manner. Note that $(\mathsf{f},\phi\vee\psi,\mathfrak{e})$ can be broken into two triples $(\mathsf{f},\phi,\mathfrak{e})$ and $(\mathsf{f},\psi,\mathfrak{e})$.

The function $\widehat{\llbracket\eta\rrbracket}$, by definition, satisfies the conditions of a measure function in all non-significant labels. In order to obtain a correct measure function, we need to make sure that these conditions are fulfilled in significant labels, too. Concretely, the algorithm has to find $c_{i}$’s such that the following inequalities hold and therefore converts each of these inequalities to a series of constraint triples.

[TABLE]

The first group of inequalities above dictate the non-negativity of the obtained measure function and the second group assure that it satisfies conditions C2’–C4’.

In this case, our algorithm creates a lot of triples and then uses Farkas lemma to simplify them and ignore triples that have contradictory preconditions or expressions that are always non-negative. Here we illustrate how some of these triples are obtained to cover the main ideas.

For example, since we must have $\widehat{\llbracket\eta\rrbracket}(\mathsf{merge},8)\geq 0$, therefore:

[TABLE]

This leads to the creation of three triples. The first part leads to

[TABLE]

and the second part leads to the following two triples that both get ignored because their expression is nonnegative even without considering the precondition: $(\mathsf{merge},i<0,0),(\mathsf{merge},j<i,0).$

As a more involved example, the following is a term in $\widehat{\llbracket\eta\rrbracket}(\mathsf{merge},2)$:

[TABLE]

here $d:=\lfloor(i+j)/2\rfloor$, $u_{3}:=\ln(d-i+1)$ and $u_{4}:=\ln(j-d).$ Note that at this stage, the term above is stored and used in its full expanded form by the algorithm and these definitions are only used in this illustration to shorten the length of this term. In step 4, the algorithm will create these variables and use the shortened representation from there on.

Since the inequality $\widehat{\llbracket\eta\rrbracket}(\mathsf{mergesort},1)\geq 1+\mathbf{1}_{1\leq i\leq j-1}\cdot\widehat{\llbracket\eta\rrbracket}(\mathsf{mergesort},2)$ should be satisfied, we get:

[TABLE]

This leads to the following constraint triples:

[TABLE]

[TABLE]

[TABLE]

The last two triples are discarded because the algorithm uses Farkas Lemma and deduces that their conditions are unsatisfiable. The first triple is also simplified using Farkas Lemma. This leads to the following final triple:

[TABLE]

All other inequalities are processed in a similar manner. In this case, at the end of this stage, the algorithm has generated 19 simplified constraint triples.

0.J.6 Step 4: Converting Constraint Triples to Linear Inequalities

This is the main step of the algorithm. Now that the triples are obtained, we need to solve the system of triples to get concrete values for $c_{i}$’s and hence upper-bounds on the runtime of functions, but this is a non-linear optimization problem. At this step, we introduce new variables and use them to obtain linear inequalities.

Step 4(a): Abstraction of Logarithmic, Exponentiation and Floored Expressions. At this stage the algorithm defines the following variables and replaces them in all constraint triples to obtain a short representation like the one we used for $\tau$:

[TABLE]

In the description we also use $w$ to denote $i+j$, but the algorithm does not add this variable. Note that all logarithmic, floored and exponentiation terms are replaced by the new variables above and hence all triples become linear, but in order for them to reflect the original triples, new conditions should be added to them. To each triple $T$, we assign a set $\Gamma$ of linear polynomials such that their non-negativity captures the desired conditions. For example, for the triple $T_{1}$ above, we have $\Gamma_{1}=\left\{i,j-i\right\}$, because the only needed conditions are $i\geq 0$ and $j\geq i$ and since no new variable has appeared in this triple, there is no need for any additional constraint.

On the other hand, for $T_{2}$, we start by setting $\Gamma_{2}=\left\{i-1,j-d-1,d-i\right\}$. Note that we could add $j-i-1$ and $i$ to $\Gamma_{2}$, too, but these can be deduced from the rest and hence the algorithm simplifies $\Gamma_{2}$ and discards them.

Since the variables $u_{0},u_{3}$ and $u_{4}$ appear in $T_{2}$ and are non-negative logarithmic terms, the algorithm adds $u_{0},u_{3},u_{4}$ to $\Gamma_{2}$.

Then the algorithm adds $w-2d=i+j-2d$ and $2d-w+1=2d-i-j+1$ to $\Gamma_{2}$. This is due to the definition of $d$ as $\lfloor w/2\rfloor$. Then it performs an emptiness checking to discard the triple if it has already become infeasible.

Step 4(b): Linear Constraints for Abstracted (Logarithmic) Variables. We find constraints for every logarithmic variable. As an example, since $j\geq d+1$ and $d\geq i$, it can be inferred that $j-i+1\geq 2$. This is the tightest obtainable bound and the algorithm finds it using Farkas Lemma. Now since $2<e$ and $u_{0}=\ln(j-i+1)$, the algorithm adds $(j-i+1)-eu_{0}$ to $\Gamma_{2}$ according to part (4) of Step 4(b). Similar constraints are added for other variables.

Next the algorithm adds constraints on the relation between $u_{i}$’s to $\Gamma_{2}$ as in parts (6) and (7). For example, since $\Gamma_{2}\geq 0$ implies $(j-i+1)-2(j-d)\geq 0$ and $2(j-d)\geq 1$, the algorithm infers that $u_{0}-\ln 2-u_{4}$ is non-negative and adds it to $\Gamma_{2}$ according to part (6).

Other constraints, and constraints for exponentiation variables, if present, will also be added according to step 4(b).

0.J.7 Step 5: Solving Unknown Coefficients in the Template ($c_{i}$’s)

After creating $\Gamma$’s, the algorithm attempts to find suitable values for the variables $c_{i}$ such that for each triple $T=(\mathsf{f},\phi,\mathfrak{e})$ and its corresponding $\Gamma$, it is the case that $\Gamma\geq 0$ implies $\mathfrak{e}\geq 0$. Since all elements of $\Gamma$ are linear, we can use Handelman’s theorem to reduce this problem to an equivalent system of linear inequalities. The algorithm does this for every triple and then appends all the resulting systems of linear inequalities together in a conjunctive manner and uses an LP-Solver to solve it. In this case the final result, obtained from lpsolve is as follows:

This means that the algorithm successfully obtained the upper-bound

[TABLE]

for the given Merge-Sort implementation.

For simplicity of illustration we do not show how to obtain a better leading constant. In the illustration above we show for constant $40.9650$, whereas our approach and implementation can obtain the constant $25.02$ (as reported in Table 1).

Appendix 0.K Experimental Details

In this part, we present the details for our experimental results.

Pseudo-codes for Our Examples. Figure 8 and Figure 9 together account for Karatsuba’s Algorithm. Figure 10 – Figure 13 demonstrate the divide-and-conquer algorithm for Closest-Pair problem. Figure 14 – Figure 16 show the Strassen’s algorithm. Invariants are bracketed (i.e., $[\dots]$) at significant labels in the programs.

Remark 6 (Approximation constants.)

We use approximation of constants upto four digits of precision. For example, we use the interval $[2.7182,2.7183]$ (resp. $[0.6931,0.6932]$) for tight approximation of $e$ (resp. $\ln{2}$). We use similar approximation for constants such as $2^{0.6}$ and $2^{0.9}$. ∎

Remark 7 (Input specifications.)

We note that as input specifications other than the input program, the invariants can be obtained automatically [18, 25]. In the examples, the invariants are even simpler, and obtained from the guards of branching labels. Besides the above we have quadruple $(d,\mathrm{op},r,k)$. We discuss these parameter for the examples below.

• •

The type of bound to be synthesized is denoted by $\mathrm{op}$: For Merge-Sort and Closest-Pair it is $\log$ (denoting logarithmic terms in expression) and for Strassen’s and Karatsuba’s algorithms, it is $\mathrm{exp}$ (denoting non-polynomial bounds with non-integral exponent).

• •

The number of terms multiplied together in each summand of the general form as in (1) is $d$. For example, (i) for $n^{4.5}$ there is only one term, and hence $d=1$; (ii) for $n^{3.9}\cdot\log n$ we have two terms, and hence $d=2$. Therefore, even for worst-case non-polynomial bounds of higher degrees, the maximum degree for template is still small. In all our examples $d$ is at most 2.

• •

Recall that $r$ is an upper bound on the degree of exponent of the asymptotic bound of the measure function. Also observe that if $r$ is not specified, we can search for $r$ in a desired interval automatically using binary search. For example, for Strassen’s algorithm, the desired interval of the exponent is between $[2,3]$. With $r=2$, our approach on Strassen’s algorithm reports failure. Thus a binary search for $r$ in the interval can obtain the exponent as $2.9$.

• •

In all our examples $k=2$ for the parameter for the Handelmann’s Theorem.

Thus the input for our algorithm is quite simple. ∎

Remark 8 (Complexity.)

Given $d$ and $k$ for the template are constants the complexity of our algorithm is polynomial. While our algorithm is exponential in these parameters, in all our examples the above parameters are at most 2. The approach we present is polynomial time (using linear programming) for several non-trivial examples, and therefore a scalable one. ∎