1 Introduction

In [2] we described an automated approach for generating loop invariants as a conjunction of polynomial equalities for a family of loops, called extended P-solvable loops. For doing so, we abstract loops to a system of algebraic recurrences over the loop counter and program variables and compute polynomial equalities among loop variables from the closed form solutions of the recurrences.

Why Julia? Our work was previously implemented in the Aligator software package [4], within the Mathematica system [8]. While Mathematica provides high-speed implementations of symbolic computation techniques, it is a proprietary software which is an obstacle for using Aligator in applications of invariant generation. The fact that Mathematica provides no possibility to parse and modify program code was also a reason to move to another environment. To make Aligator better suited for program analysis, we decided to redesign Aligator in the Julia programming language [3]. Julia provides a simple and efficient interface for calling C/C++ and Python code. This allows us to resort to already existing computer algebra libraries, such as Singular [1] and SymPy [5]. Julia also provides a built-in package manager that eases the use of other packages and enables others to use Julia packages, including our Aligator.jl tool. Before committing to Julia, we also considered the computer algebra system SageMath  [7] and an implementation directly in C/C++ as options for redesigning Aligator. The former hosts its own Python version which makes the installation of other Python packages (e.g. for parsing source code) tedious and error-prone. While C/C++ is very efficient and provides a large ecosystem on existing libraries, developing C/C++ projects requires more effort than Julia packages. We therefore believe that Julia provides the perfect mix between efficiency, extensibility and convenience in terms of programming and symbolic computations.

Aligator.jl. This paper overviews Aligator.jl and details its main components. The code of Aligator.jl is available open-source at:

https://github.com/ahumenberger/Aligator.jl.

All together, Aligator.jl consists of about 1250 lines of Julia code. We evaluated Aligator.jl on challenging benchmarks on invariant generation. Our experimental results are available at the above mentioned link and demonstrate the efficiency of Aligator.jl.

Contributions. Our new tool Aligator.jl significantly extends and improves the existing software package Aligator as follows:

  • Unlike Aligator, Aligator.jl is open-source and easy to integrate into other software packages.

  • Aligator.jl implements symbolic computation techniques directly in Julia for extracting and solving recurrences and generates polynomial dependencies among exponential sequences.

  • Contrarily to Aligator, Aligator.jl handles not only linear recurrences with constant coefficients, called C-finite recurrences. Rather, Aligator.jl also supports hypergeometric sequences and sums and term-wise products of C-finite and hypergeometric recurrences [2].

  • Aligator.jl is complete. That is, a finite basis of the polynomial invariant ideal is always computed.

2 Background and Notation

Aligator.jl computes polynomial invariants of so-called extended P-solvable loops [2]. Loop guards and test conditions are ignored in such loops and denoted by \(\ldots \) or , yielding non-deterministic loops with sequencing and conditionals. Program variables \(V=\{v_1,\ldots ,v_m\}\) of extended P-solvable loops have numeric values, abstracted to be rational numbers. The assignments of extended P-solvable loops are of the form \(v_i\mathrel {:=}\sum _{j=0}^m c_iv_j+c_{m+1}\) with constants \(c_0,\dots ,c_{m+1}\), or \(v_i\mathrel {:=}r(n)v_i\), where r(n) is a rational function in the loop counter n. We give an example of an extended P-solvable loops in Fig. 1.

Fig. 1.
figure 1

An extended P-solvable loop.

Full size image

In correspondence to \(V,\) the initial values of the variables are given by the set \(V_0:=\{v_1(0), \ldots ,v_m(0)\}\); that is, \(v_i(0)\) is the initial value of \(v_i\). In what follows, we consider V and \(V_0\) fixed and state all definitions relative to them. Given an extended P-solvable loop as input, Aligator.jl generates all its polynomial equality invariants. By a polynomial equality invariant, in the sequel simply polynomial invariant, we mean the equality:

$$\begin{aligned} p(v_1,\dots ,v_m,v_1(0),\dots ,v_m(0))=0, \end{aligned}$$
(1)

where p is a polynomial in \(V\cup V_0\) with rational number coefficients. In what follows, we also refer to the polynomial p in (1) as a polynomial invariant. For \(n\in \mathbb N\setminus \{0\}\) and a loop variable \(v_i\), we write \(v_i(n)\) to denote the value of \(v_i\) after the nth loop iteration. As (1) is a loop invariant, we have:

$$\begin{aligned} p(v_1(n),\dots ,v_m(n),v_1(0),\dots ,v_m(0))=0\text { for } n>0. \end{aligned}$$

As shown in [2, 6], the set of polynomial invariants in \(V\), w.r.t. the initial values \(V_0\), forms a polynomial ideal, called the polynomial invariant ideal. Given an extended P-solvable loop, Aligator.jl computes all its polynomial invariants as it computes a basis of the polynomial invariant ideal, a finite set of polynomials \(\{b_1,\dots ,b_k\}\). Any polynomial invariant can be written as a linear combination \(p_1b_1+\dots +p_kb_k\) for some polynomials \(p_1,\dots ,p_k\).

3 System Description of Aligator.jl

Inputs to Aligator.jl are extended P-solvable loops and are fed to Aligator.jl as in the Julia syntax. We illustrate the use of Aligator.jl on our example from Fig. 1:

Example 1

Fig. 1 is specified as a Julia string as follows:

figure a

Polynomial loop invariants are inferred using Aligator.jl by calling the function with a string input containing the loop as its argument.

figure b

The result of Aligator.jl is a Gröbner basis of the polynomial invariant ideal. It is represented as an object of type that is defined in the Singular package. For Fig. 1, Aligator.jl reports that the polynomial invariant ideal is generated by the polynomial invariant \(\{v_0^2-u_0^2-v^2+u^2+4r_0-2v_0+2 u_0 - 4 r+ 2 v - 2 u =0\}\) in variables \(r_0, v_0, u_0, r,v,u\), where \(r_0,v_0,u_0\) denote respectively the initial values of r, v, u.

We now overview the main parts of Aligator.jl: (i) extraction of recurrence equations, (ii) recurrence solving and (iii) computing the polynomial invariant ideal.

Extraction of Recurrences. Given an extended P-solvable loop as a Julia string, Aligator.jl creates the abstract syntax tree of this loop. This tree is then traversed in order to extract loop paths (in case of a multi-path loop) and the corresponding loop assignments. The resulting structure is then flattened in order to get a loop with just one layer of nested loops. Within Aligator.jl this is obtained via the method . As a result, the extracted recurrences are represented in Aligator by an object of type , in case the input is a multi-path loop; otherwise, the returned object is of type .

Example 2

Using Example 1, Aligator.jl derives the loop and its corresponding systems of recurrences:

figure c

As loop paths are translated into single-path loops, Aligator.jl introduces a loop counter for each path and computes the recurrence equations of the loop variables r, v, u with respect to the loop counters \(n_1\) and \(n_2\).

Recurrence Solving. For each single-path loop, its system of recurrences is solved. Aligator.jl performs various simplifications on the extracted recurrences, for example by eliminating cyclic dependencies introduced by auxiliary variables and uncoupling mutually dependent recurrences. The resulting, simplified recurrences represent sums and term-wise products of C-finite or hypergeometric sequences. Aligator.jl computes closed forms solutions of such recurrences by calling the method and using the symbolic manipulation capabilities of SymPy.jl:

Example 3

For Example 2, we get the following systems of closed forms:

figure d

The returned value is an array of type .

Invariant Ideal Computation. Using the closed form solutions for (each) single-path loop, Aligator.jl next derives a basis of the polynomial invariant ideal of the (multi-path) extended P-solvable loop. To this end, Aligator.jl uses the Singular.jl package for Gröbner basis computations in order to eliminate variables in the loop counter(s) from the system of closed forms. For multi-path loops, Aligator.jl relies on iterative Gröbner basis computations until a fixed point is derived representing a Gröbner basis of the polynomial invariant ideal – see [2] for theoretical details.

Computing polynomial invariants within Aligator.jl is performed by the function . The result is an object of type and represents a Gröbner basis of the polynomial invariant ideal in the loop variables.

Example 4

For Example 3, Aligator.jl generates the following Gröbner basis, as already described on page 4:

figure e

4 Experimental Evaluation

Our approach to invariant generation was shown to outperform state-of-the-art tools on invariant generation for multi-path loops with polynomial arithmetic [2]. In this section we focus on the performance of our new implementation in Aligator.jl and compare results to Aligator  [4]. In our experiments, we used benchmarks from [2]. Our experiments were performed on a machine with a 2.9 GHz Intel Core i5 and 16 GB LPDDR3 RAM. When using Aligator.jl, the invariant ideal computed by Aligator.jl was non-empty for each example; that is, for each example we were able to find non-trivial invariants.

Tables 1(a) and (b) show the results for a set of single- and multi-path loops respectively. In both tables the first column shows the name of the instance, whereas columns two and three depict the running times (in seconds) of Aligator and Aligator.jl, respectively.

Table 1. Experimental evaluation of Aligator.jl.
Full size table

By design, Aligator.jl is at least as strong as Aligator concerning the quality of the output. When it comes to efficiency though, we note that Aligator.jl is slower than Aligator. We expected this result as Aligator uses the highly optimized algorithms of Mathematica. When taking a closer look at how much time is spent in the different parts of Aligator.jl, we observed that the most time in Aligator.jl is consumed by symbolic manipulations. Experiments indicate that we can improve the performance of Aligator.jl considerably by using the Julia package SymEngine.jl instead of SymPy.jl. We believe that our initial experiments with Aligator.jl are promising and demonstrate the use of our efforts in making our invariant generation open-source.

5 Conclusion

We introduced the new package Aligator.jl for loop invariant generation in the programming language Julia. Our Aligator.jl tool is an open-source software package for invariant generation using symbolic computation and can easily be integrated with other libraries and tools.