Parameterized Recursive Refinement Types for Automated Program Verification

Abstract

Refinement types have recently been applied to program verification, where program verification problems are reduced to type checking or inference problems. For fully automated verification of programs with recursive data structures, however, previous refinement type systems have not been satisfactory: they were not expressive enough to state complex properties of data, such as the length and monotonicity of a list, or required explicit declarations of precise types by users. To address the problem above, we introduce parameterized recursive refinement types (PRRT), which are recursive datatypes parameterized by integer parameters and refinement predicates; those parameters can be used to express various properties of data structures such as the length/sortedness of a list and the depth/size of a tree. We propose an automated type inference algorithm for PRRT, by a reduction to the satisfiability problem for CHCs (Constrained Horn Clauses). We have implemented a prototype verification tool and evaluated the effectiveness of the proposed method through experiments.

1 Introduction

There has been a lot of progress on automated/semi-automated verification techniques for functional programs, such as those based on higher-order model checking [6, 14, 16] and refinement types [2, 15, 17, 18, 20,21,22, 24, 25]. Fully automated verification of functional programs using recursive data structures, however, still remains a challenge. In the present paper, we follow the approach using refinement types, and introduce parameterized recursive refinement types and a type inference procedure for them.

Refinement types can be used to express various properties of recursive data types. For example, if we are interested in the length of an integer list, we can prepare a type of the form $\texttt{ilistL}[n]$, which describes a list of length n, and assign the following types to constructors:

$$\begin{aligned}&\texttt{Nil}: \texttt{ilistL}[0]\\&\texttt{Cons}: \forall n.\texttt{int}\times \texttt{ilistL}[n]\rightarrow \texttt{ilistL}[n+1] \end{aligned}$$

The type of $\texttt{Cons}$ indicates that $\texttt{Cons}$ takes a pair consisting of an integer and a list of length $n$ as an argument, and returns a list of length $n+1$. If we are interested in the sortedness of a list (in the ascending order) instead, we may prepare a type of the form $\texttt{ilistS}[b,x]$, which describes a list consisting of elements no less than $x$, where the additional Boolean parameter $b$ denotes whether the list is null (thus, if $b$ is true, the value of $x$ should be ignored). The following types can then be assigned to the constructors. (Actually, the second parameter $0$ of the type of $\texttt{Nil}$ does not matter and may be any other value.)

$$\begin{aligned}&\texttt{Nil}: \texttt{ilistS}[\texttt{true},0]\\&\texttt{Cons}: \forall b,x,y.\;x\mathbin {:}\texttt{int}\times \{\texttt{ilistS}[b,y]\mid \lnot b\Rightarrow x\le y\}\rightarrow \texttt{ilistS}[\texttt{false},x] \end{aligned}$$

Once an appropriate refinement type is assigned to each occurrence of a constructor, a standard procedure for automated/semi-automated refinement type inference (e.g., based on a reduction to the CHC solving problem [2, 15, 18, 25]) is applicable.

A main problem in applying the refinement type approach above to the fully-automated verification is that each constructor has more than one refinement type, and it is unclear which type should be used for each occurrence of the constructor (unless a programmer explicitly declares it). For example, for a sorting function $\texttt{sort}$, an input list is a plain, unsorted list, while the output list should be sorted; hence the latter should have type $\texttt{ilistS}[b,x]$ for some $b,x$. In the context of fully automated verification, we cannot expect a programmer to declare the types like $\texttt{ilistL}[n]$ and $\texttt{ilistS}[b,x]$ above. Thus, an automated verification tool should choose appropriate refinements of recursive data types from infinitely many candidates.

To address the problem above, we parameterize recursive types with integers and predicates, and assign generic types to data type constructors. For example, for integer lists, we prepare a parameterized type $\texttt{ilist}\langle {n; e_\texttt{Nil}, (\varphi _{\texttt{Cons}},{e_{\texttt{Cons}}})}\rangle$, where $n$ is an integer denoting the number of integer parameters, $\varphi _{\texttt{Cons}}$ is a predicate on integers, and $e_\texttt{Nil}$ and $e_{\texttt{Cons}}$ are functions on integer tuples, and we assign the following types to constructors:

$$\begin{aligned}&\texttt{Nil}: \forall k,P_\texttt{Cons}, f_\texttt{Nil}, f_\texttt{Cons}. \texttt{ilist}\langle {k;f_\texttt{Nil}, (P_\texttt{Cons},f_\texttt{Cons})}\rangle [f_\texttt{Nil}()]\\&\texttt{Cons}: \forall k,P_\texttt{Cons}, f_\texttt{Nil}, f_\texttt{Cons}. \forall \widetilde{y}. \\ {}&\qquad \{x\mathbin {:}\texttt{int}\times \texttt{ilist}\langle {k;f_\texttt{Nil},(P_\texttt{Cons},f_\texttt{Cons})}\rangle [\widetilde{y}]\mid P_\texttt{Cons}(x,\widetilde{y})\} \\ {}&\qquad \qquad \qquad \qquad \rightarrow \texttt{ilist}\langle {k;f_\texttt{Nil},(P_\texttt{Cons},f_\texttt{Cons})}\rangle [{f}_\texttt{Cons}(x,\widetilde{y})] \end{aligned}$$

Here, (i) $P_\texttt{Cons}$ is a predicate variable, (ii) $f_\texttt{Nil}$ and $f_\texttt{Cons}$ are functions of types $\texttt{unit}\rightarrow \texttt{int}^k$ and $\texttt{int}^{k+1}\rightarrow \texttt{int}^k$ respectively, and (iii) $\widetilde{y}$ is a sequence of $k$ integer variables (where $k$ is the first parameter of $\texttt{ilist}$). By changing the part $\langle {k;f_\texttt{Nil},(P_\texttt{Cons},f_\texttt{Cons})}\rangle$, we can express various list properties. For example, list type constructors $\texttt{ilistL}$ and $\texttt{ilistS}$ can be defined as follows:

$$\begin{aligned}&\texttt{ilistL}:= \texttt{ilist}\langle {1;\lambda ().0, (\lambda (x,y).\texttt{true}, \lambda (x,y).y+1)}\rangle \\&\texttt{ilistS}:= \texttt{ilist}\langle {2;\lambda ().(0,0), (\lambda (x,y_1,y_2).y_1>0 \Rightarrow x\le y_2, \lambda (x,y_1,y_2). (1, x))}\rangle . \end{aligned}$$

In fact, by instantiating the parameters $k,P_\texttt{Cons},f_\texttt{Nil}$ and $f_\texttt{Cons}$ to $1$, $\lambda (x,y).\texttt{true}$, $\lambda ().0$, and $\lambda (x,y).y+1$ respectively, we obtain the following types for $\texttt{Nil}$ and $\texttt{Cons}$:

$$\begin{aligned}&\texttt{Nil}\mathbin {:}\texttt{ilistL}[0]\\&\texttt{Cons}\mathbin {:}\forall y. \{x\mathbin {:}\texttt{int}\times \texttt{ilistL}[y]\mid \texttt{true}\}\rightarrow \texttt{ilistL}[y+1], \end{aligned}$$

which corresponds to the types of $\texttt{Nil}$ and $\texttt{Cons}$ given for $\texttt{ilistL}$. Similarly, by instantiating the parameters $k,P_\texttt{Cons},f_\texttt{Nil}$ and $f_\texttt{Cons}$ to $2, \lambda (x,y_1,y_2).y_1>0 \Rightarrow x\le y_2, \lambda ().(0,0)$, and $\lambda (x,y_1,y_2). (1, x)$ respectively, we obtain the types of $\texttt{Nil}$ and $\texttt{Cons}$ given for $\texttt{ilistS}$.

The remaining question is how to automatically assign an appropriate instantiation of parameterized recursive types to each occurrence of a constructor. To this end, we first pick the values of $k, f_\texttt{Nil}, f_\texttt{Cons}$ (in the case of lists; we will deal with more general recursive data types in the following sections) in a certain heuristic manner, and prepare a predicate variable for $P_\texttt{Cons}$. We can then reduce the problem of refinement type inference to the CHC satisfiability problem [1] in a standard manner [2, 18], and use an automated CHC solver [2, 4, 7]. If the refinement type inference fails, that may be due to the lack of sufficient parameters; thus, we increase the value of $k$ and accordingly update the guess for $f_\texttt{Nil}$ and $f_\texttt{Cons}$ so that the resulting refinement types are strictly more expressive. This refinement loop may not terminate due to the incompleteness of the type system discussed later in Sect. 3, but we can guarantee a weak form of relative completeness, that if a program is typable, then the type inference procedure terminates eventually under the hypothetical completeness assumption of the underlying CHC solver, as discussed later in Sect. 4.

We have implemented the procedure sketched above, and succeeded in fully automatic verification of several small but challenging programs using lists and trees. Our contributions are summarized as follows.

• The design of parameterized recursive refinement types (PRRT): the idea of parameterizing recursive types with some indices goes back at least to Xi and Pfenning’s work [24], and that of parameterization of types with refinement predicates has also been proposed by Vazou et al. [21]. We believe, however, that the specific combination of the parameterizations, specifically designed with fully automated verification in mind, is new.

• An inference procedure for PRRTs, its implementation and experiments.

The rest of this paper is structured as follows. Section 2 introduces the target language of our verification method based on parameterized recursive refinement types. Section 3 proposes a new refinement type system, and Sect. 4 explains a type inference procedure, which serves as a program verification procedure. Section 5 reports an implementation and experimental results. Section 6 discusses related work, and Sect. 7 concludes the paper.

2 Target Language

We consider a first-order¹ call-by-value functional language as the target of our refinement type inference.

2.1 Syntax

We assume a finite set of data constructors, ranged over by $L$. The set of expressions, ranged over by $e$, is defined by:

$$\begin{aligned} e \text{(expressions) } {:}{:=\;}\;&s \mid f(\widetilde{s}) \mid \texttt{fail}\mid \texttt{if}\ s\ \texttt{then}\ {e_1}\ \texttt{else}\ {e_2}\\ \mid \;&\texttt{let}\ x=e_1\ \texttt{in}\ {e_2}\\ \mid \;&\texttt{match}\ {s}\ \texttt{with}\ \{L_1(\widetilde{x}_1)\rightarrow e_1, \ldots ,L_k(\widetilde{x}_k)\rightarrow e_k\}\\ s \text{(simple } \text{ expressions) } {:}{:=\;}\;&x \mid n \mid s_1+s_2\mid L(s_1,\ldots ,s_k)\\ D \text{(programs) } {:}{:=\;}\;&\{f_1(\widetilde{x}_1)=e_1,\ldots ,f_k(\widetilde{x}_k)=e_k\} \end{aligned}$$

The syntax of expressions above is fairly standard. A simple expression denotes an integer or a recursive data structure; we represent Booleans as integers, where non-zero integers are considered $\texttt{true}$ and $0$ is considered $\texttt{false}$. We write $\widetilde{\cdot }$ for a sequence; for example, $\widetilde{s}$ denotes a sequence of simple expressions $s_1,\ldots ,s_k$. For a technical convenience, the arguments of a function call $f(\widetilde{s})$ are restricted to simple expressions; this is not a fundamental restriction, $f\,e$ can be expressed by $\texttt{let}\ x=e\ \texttt{in}\ {f\,x}$. The expression $\texttt{fail}$ is a special command to indicate an error; the purpose of our refinement type system introduced later is to guarantee that $\texttt{fail}$ does not occur during the execution of any well-typed program. As demonstrated in the examples below, the expression $\texttt{fail}$ is often used to express the specification of a program. The conditional expression $\texttt{if}\ s\ \texttt{then}\ {e_1}\ \texttt{else}\ {e_2}$ evaluates $e_2$ if the value of $s$ is $0$ and evaluates $e_1$ otherwise. The match expression $\texttt{match}\ {s}\ \texttt{with}\ \{L_1(\widetilde{x}_1)\rightarrow e_1, \ldots ,L_k(\widetilde{x}_k)\rightarrow e_k\}$ evaluates $[\widetilde{v}_i/\widetilde{x}_i]e_i$ if the value of $s$ is $L_i(\widetilde{v}_i)$. For the sake of simplicity, we have only $+$ as an operator on integers, but other standard primitives (−, $\times$, <, $=$, ...) can be incorporated with no difficulty, and used in examples.

A program $D$ is a set of (mutually recursive) function definitions. We assume that the set $\{f_1,\ldots ,f_k\}$ of function names contains $\texttt{main}$, the name of the “main” function.

2.2 Typing

We introduce a simple (monomorphic) type system, and require that programs and expressions are well-typed in the type system.

We assume a finite set $\mathcal {D}$ of (names of) recursive data types, ranged over by $\texttt{d}$. The set of (simple) types, ranged over by $\kappa$, is defined by:

$$\begin{aligned} \kappa \text{(simple } \text{ types) } {:}{:=\;}\;&b\mid (b_1, \ldots , b_k) \rightarrow b\\ b \text{(base } \text{ types) } {:}{:=\;}\;&\texttt{int}\mid \texttt{d}\end{aligned}$$

Here, a type of the form $(b_1,\ldots ,b_k)\rightarrow \texttt{d}$ is called a constructor type. When $k=1$, we just write $b\rightarrow \texttt{d}$ for $(b)\rightarrow \texttt{d}$. To distinguish simple types from refinement types introduced later, we sometimes call simple types sorts.

A constructor environment, written $\mathcal {C}$, is a map from the set of data constructor to the set of constructor types. A (simple) type environment, written $\mathcal {K}$, is a map from a finite set of variables to types. The type judgment relations $\mathcal {C};\mathcal {K}\vdash _{\texttt{ST}}e:\kappa$ and $\mathcal {C}\vdash _{\texttt{ST}}D:\mathcal {K}$ are defined by the typing rules in Fig. 1.

Henceforth, we consider only expressions $e$ and programs $D$ such that $\mathcal {C};\mathcal {K}\vdash _{\texttt{ST}}e:\kappa$ and $\mathcal {C}\vdash _{\texttt{ST}}D:\mathcal {K}$ for some $\mathcal {C}, \mathcal {K}$. As usual, programs well-typed in the simple type system do not get stuck; however, they may be reduced to the error state $\texttt{fail}$.

In the rest of this paper, we further impose the following restriction on constructor types: for each constructor type $\mathcal {C}(L)=(b_1,\ldots ,b_k)\rightarrow \texttt{d}$, we require that $\{b_1,\ldots ,b_k\}\subseteq \{\texttt{int},\texttt{d}\}$. Thus, we forbid a constructor type like $(\texttt{int},\texttt{d}_1)\rightarrow \texttt{d}_2$ with $\texttt{d}_1\ne \texttt{d}_2$. We permute argument types and normalize each constructor type to the form $(\texttt{int}^{k},\texttt{d}^\ell )\rightarrow \texttt{d}$. Again, the restriction is just for the sake of simplicity of the discussions in later sections. We write $\mathcal {C}_\texttt{d}$ for the restriction of $\mathcal {C}$ on type $\texttt{d}$, $\{L\mathbin {:}\kappa \in \mathcal {C}\mid \kappa \text{ is } \text{ of } \text{ the } \text{ form } (\widetilde{b})\rightarrow \texttt{d}\}$. Note that $\mathcal {C}$ can be decomposed to the disjoint union of maps $\mathcal {C}_{\texttt{d}_1}\uplus \cdots \uplus \mathcal {C}_{\texttt{d}_k}$. For the integer list type $\texttt{ilist}$ discussed in Sect. 1, $\mathcal {C}_{\texttt{ilist}} = \{\texttt{Nil}\mapsto (\,)\rightarrow \texttt{ilist}, \texttt{Cons}\mapsto (\texttt{int},\texttt{ilist})\rightarrow \texttt{ilist}\}$.

Fig. 1.

Simple Type System

2.3 Operational Semantics

We define a small-step semantics of the language. The sets of evaluation contexts and values, respectively ranged over by $E$ and $v$, are defined by:

$$\begin{aligned} E{:}{:=\;}\;&[\,]\mid E+s\mid n+E\mid L(\widetilde{v},E,\widetilde{s})\mid f(\widetilde{v},E,\widetilde{s}) \mid \texttt{if}\ E\ \texttt{then}\ {e_1}\ \texttt{else}\ {e_2}\\ \mid \;&\texttt{let}\ x=E\ \texttt{in}\ {e} \mid \texttt{match}\ {E}\ \texttt{with}\ \{L_1(\widetilde{x}_1)\rightarrow e_1, \ldots ,L_k(\widetilde{x}_k)\rightarrow e_k\}\\ v {:}{:=\;}\;&n \mid L(v_1,\ldots ,v_k)\\ \end{aligned}$$

The reduction relation $e\longrightarrow _{D} e'$ on (closed) expressions is defined by the rules in Fig. 2. The expression $[\widetilde{v}/\widetilde{x}]e$ (which is an abbreviated form of $[v_1/x_1,\ldots ,v_k/x_k]e$) denotes the expression obtained from $e$ by substituting $\widetilde{v}$ for $\widetilde{x}$. We write $\longrightarrow ^*_{D}$ for the reflexive and transitive closure of $\longrightarrow _{D}$. We sometimes omit the subscript $D$ and just write $\longrightarrow {}$ and $\longrightarrow ^*{}$ for $\longrightarrow _{D}$ and $\longrightarrow ^*_{D}$ respectively.

For a program $D$ such that $\mathcal {C}\vdash _{\texttt{ST}}D:\mathcal {K}$ and $\mathcal {K}(\texttt{main})=(b_1,\ldots ,b_k)\rightarrow \texttt{int}$, we say $D$ is safe if there exist no $v_1\mathbin {:}b_1,\ldots ,v_k\mathbin {:}b_k$ and $E$ such that $\texttt{main}(v_1,\ldots ,v_k)\longrightarrow ^*_{D} E[\texttt{fail}]$. In the rest of this paper, we shall develop a refinement type system that guarantees the safety of any well-typed program, and an automated procedure for proving the well-typedness, hence the safety of a given program. Note that the safety of a program does not imply the termination of the program; termination verification, for which various techniques [8, 9] are available, is outside the scope of this paper.

Fig. 2.

Reduction Rules

Example 1

The program $D_1$ defined below declares function $\texttt{range}$, which takes an integer n and returns the list $[n, n-1, \ldots , 1]$, and checks that the length of $\texttt{range}(n)$ equals its argument n.

$$\begin{aligned} D_1 = \{&\texttt{range}(n) = \texttt{if}\ n \ \texttt{then}\ \texttt{let}\ r=\texttt{range}(n - 1)\ \texttt{in}\ {\texttt{Cons}(n, r)} \\&\qquad \qquad \quad \texttt{else}\ {\texttt{Nil}()}, \\&\texttt{len}(l) = \texttt{match}\ {l}\ \texttt{with}\ \{\texttt{Nil}() \rightarrow 0,\ \texttt{Cons}(n, l^\prime ) \rightarrow 1 + \texttt{len}(l^\prime )\}, \\&\texttt{main}(n) = \texttt{let}\ r=\texttt{range}(n)\ \texttt{in}\ {\texttt{let}\ l=\texttt{len}(r)\ \texttt{in}\ {}} \\&\qquad \qquad \qquad \quad \texttt{if}\ n \ne l\ \texttt{then}\ {\texttt{fail}}\ \texttt{else}\ {0} \} \end{aligned}$$

The evaluation of $\texttt{main}(n)$ terminates without failure if $n \ge 0$, and falls into an infinite loop if $n<0$.    $\square$

Example 2

The following program $D_2$ focuses on function $\texttt{isort}$, which sorts a list in the ascending order by the insertion sort algorithm, and checks that its return value is sorted.

$$\begin{aligned} D_2 = \{&\texttt{gen}(n) = \texttt{if}\ n\ \texttt{then}\ {\texttt{Cons}(*, \texttt{gen}(n - 1))}\ \texttt{else}\ {\texttt{Nil}()}, \\&\begin{array}{l}\! \texttt{insert}(x, l) = \texttt{match}\ {l}\ \texttt{with}\ \{ \\ \qquad \texttt{Nil}() \rightarrow \texttt{Cons}(x, \texttt{Nil}()), \\ \qquad \texttt{Cons}(y, l') \rightarrow \texttt{if}\ x < y\ \texttt{then}\ {\texttt{Cons}(x, l)}\ \texttt{else}\ {\texttt{Cons}(y, \texttt{insert}(x, l'))} \\ \}, \end{array} \\&\begin{array}{l}\! \texttt{isort}(l) = \texttt{match}\ {l}\ \texttt{with}\ \{ \\ \qquad \texttt{Nil}() \rightarrow \texttt{Nil}(),\ \texttt{Cons}(n, l^\prime ) \rightarrow \texttt{insert}(n, \texttt{isort}(l^\prime )) \\ \}, \end{array} \\&\begin{array}{l}\! \mathtt {is\_sorted\_rec}(x, l) = \texttt{match}\ {l}\ \texttt{with}\ \{ \\ \qquad \texttt{Nil}() \rightarrow 1, \\ \qquad \texttt{Cons}(y, l^\prime ) \rightarrow \texttt{if}\ x \le y\ \texttt{then}\ {\mathtt {is\_sorted\_rec}(y, l^\prime )}\ \texttt{else}\ {0} \\ \}, \end{array} \\&\begin{array}{l}\! \mathtt {is\_sorted}(l) = \texttt{match}\ {l}\ \texttt{with}\ \{ \\ \qquad \texttt{Nil}() \rightarrow 1,\ \texttt{Cons}(n, l^\prime ) \rightarrow \mathtt {is\_sorted\_rec}(n, l^\prime ) \\ \}, \end{array} \\&\texttt{main}(n) = \begin{array}{l} \texttt{let}\ s=\mathtt {is\_sorted}(\texttt{isort}(\texttt{gen}(n)))\ \texttt{in}\ {} \\ \texttt{if}\ s\ \texttt{then}\ {0}\ \texttt{else}\ {\texttt{fail}} \end{array} \\ \} \end{aligned}$$

The term $*$ indicates a non-deterministic integer value, omitted in the formal syntax for the sake of simplicity. The function $\texttt{insert}$ constitutes a part of the insertion sort, which takes x and a sorted list l and returns a sorted list that consists of x and the elements of l. The function $\mathtt {is\_sorted}$ returns 1 if the given list is sorted in the ascending order, and 0 otherwise.    $\square$

Example 3

The type $\texttt{itree}$ for binary trees with integer values is defined with $\mathcal {C}_{\texttt{itree}} = \{ \texttt{Leaf}\mapsto (\,) \rightarrow \texttt{itree}, \texttt{Node}\mapsto (\texttt{int},\texttt{itree},\texttt{itree}) \rightarrow \texttt{itree}\}$. The following program $D_3$ generates a random tree with a given size, and verifies that the generated tree has the given size as expected.

$$\begin{aligned} D_3 = \{&\begin{array}{l} \mathtt {gen\_tree}(n) = \\ \quad \texttt{if}\ n\ \texttt{then} \\ \qquad \texttt{let}\ m=*\ \texttt{in}\ {\texttt{let}\ \ell =\mathtt {gen\_tree}(m)\ \texttt{in}\ {}} \\ \qquad \texttt{let}\ r=\mathtt {gen\_tree}(n - 1 - m)\ \texttt{in}\ { \texttt{Node}(*, l, r)} \\ \quad \texttt{else}\ \texttt{Nil}(), \end{array} \\&\begin{array}{l}\! \texttt{size}(t) = \texttt{match}\ {t}\ \texttt{with}\ \{ \\ \qquad \texttt{Leaf}() \rightarrow 0, \\ \qquad \texttt{Node}(\_, \ell , r) \rightarrow 1 + \texttt{size}(\ell ) + \texttt{size}(r) \\ \}, \end{array} \\&\texttt{main}(n) = \begin{array}{l} \texttt{let}\ s=\texttt{size}(\mathtt {gen\_tree}(n))\ \texttt{in}\ {} \\ \texttt{if}\ s \ne n\ \texttt{then}\ {\texttt{fail}}\ \texttt{else}\ {0} \end{array} \\ \}. \end{aligned}$$

If $n\ne 0$,² $\mathtt {gen\_tree}(n)$ picks a number $m$, and returns a tree of size $n$, consisting of the left child of size $m$ and the right child of size $n-1-m$. Function $\texttt{size}$ calculates the tree size (the number of nodes except leaves).    $\square$

3 A Parameterized Refinement Type System

This section introduces a refinement type system that guarantees the safety of well-typed programs.

3.1 Refinement Types

The syntax of parameterized recursive refinement types, ranged over by $\tau$, is defined by:

$$\begin{aligned} \tau \text{(types) }&{:}{:=\;} \{\beta \mid \varphi \} \mid \{(\beta _1,\ldots ,\beta _k)\mid \varphi '\}\rightarrow \{\beta \mid \varphi \}\\ \beta \text{(type } \text{ patterns) }&{:}{:=\;} \delta [y_1,\ldots ,y_n]\\ \delta \text{(raw } \text{ types) }&{:}{:=\;} \texttt{int}\mid \texttt{d}\langle {n;(P_1,F_1),\ldots , (P_k,F_k)}\rangle \\ P \text{(predicates) }&{:}{:=\;} \lambda (\widetilde{y}).\varphi \end{aligned}$$

Here, $\varphi$ denotes a formula over integer arithmetic, and $F$ denotes a function on integer tuples; we do not fix the precise syntax of $\varphi$ and $F$, but assume that standard arithmetic and logical operators are available. In $\delta [y_1,\ldots ,y_n]$, (i) $n=1$ if the raw type $\delta$ is $\texttt{int}$, and (ii) $n=m$ if $\delta =\texttt{d}\langle {m;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle$. Intuitively, $\{\texttt{int}[x] \mid \varphi \}$ is the type of an integer $x$ that satisfies $\varphi$. The type $\{(\beta _1,\ldots ,\beta _k)\mid \varphi '\}\rightarrow \{\beta \mid \varphi \}$ describes a function or a constructor that takes arguments of types $\beta _1,\ldots ,\beta _k$ that satisfy $\varphi '$, and returns a value of type $\{\beta \mid \varphi \}$. For example, $\{(\texttt{int}[x])\mid x>0\}\rightarrow \{\texttt{int}[y]\mid y>x\}$ describes a function that takes a positive integer $x$ as an argument and returns an integer greater than $x$. As this example indicates, the variables occurring in the part $(\beta _1,\ldots ,\beta _k)$ are bound in $\{(\beta _1,\ldots ,\beta _k)\mid \varphi '\}\rightarrow \{\beta \mid \varphi \}$, and may occur in $\varphi '$ and $\varphi$. As usual, we allow implicit renaming of bound variables. We often write $\delta ^![s_1,\ldots ,s_n]$ for $\{\delta [y_1,\ldots ,y_n]\mid y_1=s_1\wedge \cdots \wedge y_n=s_n\}$; we sometimes omit the superscript $!$ when there is no danger of confusion.

Refinement types for datatypes are more involved. For each (simple) datatype $\texttt{d}$ with $\mathcal {C}_\texttt{d}=\{L_1\mathbin {:}(\texttt{int}^{\ell _1},\texttt{d}^{m_1})\rightarrow \texttt{d},\ldots , L_k\mathbin {:}(\texttt{int}^{\ell _k},\texttt{d}^{m_k})\rightarrow \texttt{d}\}$, we consider refinement types of the form:

$$ \{\texttt{d}\langle {n; (P_1,F_1),\ldots ,(P_k,F_k)}\rangle [y_1,\ldots ,y_n] \mid \varphi \}. $$

Here, $n$ denotes the number of integer parameters $y_1,\ldots ,y_n$, and $(P_i,F_i)$ is a pair of a predicate and a function corresponding to the constructor $L_i$. The above type denotes a data structure constructed from $L_1,\ldots ,L_k$, by assigning the following type to $L_i$.

$$\begin{aligned} \{(\texttt{int}[x_1],\ldots ,\texttt{int}[x_{\ell _i}],\delta [\widetilde{y}_1],\ldots ,\delta [\widetilde{y}_{m_i}])&\mid P_i(\widetilde{x},\widetilde{y}_1,\ldots ,\widetilde{y}_{m_i})\} \\ \rightarrow \;&\delta ^![F_i(\widetilde{x},\widetilde{y}_1,\ldots ,\widetilde{y}_{m_i})] \end{aligned}$$

Here, $\delta$ denotes $\texttt{d}\langle {n; (P_1,F_1),\ldots ,(P_k,F_k)}\rangle$, $\widetilde{x}=x_1,\ldots ,x_{\ell _i}$, and $\widetilde{y}_i = y_{i,1},\ldots ,y_{i,n}$. Thus, the arity of the predicate $P_i$ and the function $F_i$ is $\ell _i+m_in$, and $F_i$ returns an $n$-tuple of integers. Recall that the part $\delta ^![F_i(\widetilde{x},\widetilde{y}_1,\ldots ,\widetilde{y}_{m_i})]$ should be considered an abbreviated form of $\{\delta [z_1,\ldots ,z_n]\mid (z_1,\ldots ,z_n)= F_i(\widetilde{x},\widetilde{y}_1,\ldots ,\widetilde{y}_{m_i})\}$. Note that $P_i$ and $F_i$ take only integers as their arguments; thus information about recursive data structures is abstracted to integers by the type system.

For example, $\texttt{ilistL}$ in Sect. 1 is expressed as

$$\texttt{ilist}\langle {1;(\lambda ().\texttt{true},\lambda ().0), (\lambda (x,y).\texttt{true}, \lambda (x,y).y+1)}\rangle ,$$

and the constructors $\texttt{Nil}$ and $\texttt{Cons}$ are given the following types:

$$\begin{aligned}&\texttt{Nil}\mathbin {:}(\,)\rightarrow \texttt{ilistL}^![0]\\&\texttt{Cons}\mathbin {:}(\texttt{int}[x],\texttt{ilistL}[y])\rightarrow \texttt{ilistL}^![y+1]. \end{aligned}$$

Note that the argument type of $\texttt{Cons}$ is

$$\{(\texttt{int}[x],\texttt{ilistL}[y])\mid (\lambda (x,y).\texttt{true})(x,y)\} \equiv \{(\texttt{int}[x],\texttt{ilistL}[y])\mid \texttt{true}\},$$

which has been abbreviated to $(\texttt{int}[x],\texttt{ilistL}[y])$.

As another example, recall $\texttt{ilistS}$ in Sect. 1. It is expressed as:

$$\begin{aligned} \texttt{ilist}\langle 2;&(\lambda (\,).\texttt{true}, \lambda (\,).(0,0)),\\ {}&(\lambda (x,y_1,y_2).(y_1>0\Rightarrow x\le y_2), \lambda (x,y_1,y_2).(1, x))\rangle , \end{aligned}$$

and the constructors are given the following types:

$$\begin{aligned}&\texttt{Nil}\mathbin {:}(\,)\rightarrow \texttt{ilistS}^![0,0]\\&\texttt{Cons}\mathbin {:}\{(\texttt{int}[x],\texttt{ilistS}[y_1,y_2])\mid y_1>0\Rightarrow x\le y_2\} \rightarrow \texttt{ilistS}^![1, x]. \end{aligned}$$

Remark 1

If we are interested in proving that a sorting function takes an integer list as an argument and returns a sorted list that is a permutation of the argument, we need to parameterize the list type also with information about the elements of a list. One way to do so would be to introduce the type $\texttt{ilistP}[y_1,y_2,y_3]$ of a list of length $y_1$ that contains $y_3$ occurrences of the element $y_2$, and the type $\texttt{ilistSP}[y_1,y_2,y_3,y_4]$ of a sorted list (of type $\texttt{ilistS}[y_1,y_2]$) containing $y_4$ occurrences of the element $y_3$. Then the type of a sorting function can be expressed as: $\{\texttt{ilistP}[y_1,y_2,y_3]\mid \texttt{true}\}\rightarrow \{\texttt{ilistSP}[y_1,z,y_2,y_3]\mid \texttt{true}\}$.    $\square$

3.2 Typing

We define the type judgment relations $\mathcal {C};\varGamma ;\varphi \vdash e:\tau$ and $\mathcal {C}\vdash D:\varGamma$ for expressions and programs by the typing rules in Fig. 3. Here, $\mathcal {C}$ is a constructor type environment as before, and $\varGamma$ maps each variable (including a function name) to its type. The type bindings on integer types and datatypes are restricted to the form $x\mathbin {:}\{\beta \mid \texttt{true}\}$, so we just write $x\mathbin {:}\beta$. The conditions on variables of integer types and datatypes are instead accumulated in the part $\varphi$ of the type environment. Type bindings on integer types are further restricted to $x\mathbin {:}\texttt{int}[x]$; hence we sometimes just write $x\mathbin {:}\texttt{int}$. In a type judgment $\mathcal {C};\varGamma ;\varphi \vdash e:\tau$, we implicitly require that all the types are well-formed; for example, $\varphi$ and $\tau$ may contain only integer variables occurring in $\varGamma$ (including those in the part $\beta$) as free variables. The definition of well-formedness is given in the longer version of this paper [13].

The type judgment $\mathcal {C};\varGamma ;\varphi \vdash e:\tau$ intuitively means that if each free variable in $e$ has type $\varGamma (x)$ and satisfies the condition described by $\varphi$, then $e$ is safely executed (without reaching $\texttt{fail}$), and either $e$ diverges or evaluates to a value of type $\tau$. In Fig. 3, $\models \varphi$ means that the formula $\varphi$ is a valid formula of integer arithmetic.

Fig. 3.

Refinement Type System

We explain some key rules. The typing rules for expressions are fairly standard, except T-DC and T-Sub for datatypes. In T-App, we require that the $\beta$-part of the argument types matches between the function and actual arguments. The condition $\models \varphi \wedge (\bigwedge _{i=1}^{k} \varphi _i ) \Rightarrow \varphi '$ requires that the condition $\varphi '$ required by the function is met by the actual arguments. In rule T-Fail, the condition $\models \lnot \varphi$ ensures that there exists no environment that makes $\varphi$ hold, so that $\texttt{fail}$ is unreachable. In T-If, the branching condition is accumulated in the conditions for the then- and else-branches. In T-Let, the condition $\varphi _1$ on the value of $e_1$ is accumulated in the condition for $e_2$.

In rule T-DC, the third and fourth conditions require that the arguments of the constructor $L_i$ has an appropriate type, and the fifth condition requires that they also satisfy the precondition $P_i$. The last premise ensures the post condition (represented by the function $F_i$) of the data constructor implies the condition $\varphi '$ on the constructed data. Note that the “$\delta$-part” may be locally chosen in the rule (thus, the constructor $L_i$ is polymorphic on $\langle {n;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle$, and that part may be instantiated for each occurrence of the constructor), but that the same $\delta$ must be used among $L_i(s_1,\ldots ,s_{\ell _i+m_i})$ and the components $s_{\ell _i+1},\ldots ,s_{\ell _i+m_i}$.

In rule T-Match, the type environment $\varGamma '_i$ for the subexpression $e_i$ is obtained from $\varGamma$ by adding type bindings for the variables $\widetilde{x}_i$ (see the fourth line of the premises). The condition $\varphi _i'$ (defined on the fifth line) is obtained by strengthening the condition $\varphi$ with information that $s$ matches $L_i(\widetilde{x}_i)$. Note that as in rule T-DC, the “$\delta$-part” is shared among $s$ and decomposed elements (bound to) $x_{\ell _i+1},\ldots ,x_{\ell _i+m_i}$. The rule T-Sub is for subsumption. We allow only the refinement condition to be weakened; for datatypes, the $\beta$-part (of the form $\texttt{d}\langle {n;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle [\widetilde{y}]$) is fixed.

Example 4

Let us recall the program $D_1$ defined in Example 1. It is typed as $\mathcal {C}\vdash D_1: \varGamma _0$, where $\varGamma _0$ consists of:

$$\begin{aligned}&\texttt{range}\!: \texttt{int}[n] \rightarrow \texttt{ilistL}^![n],\\&\texttt{len}\!: \texttt{ilistL}[n] \rightarrow \texttt{int}^![n],\\&\texttt{main}\!: \texttt{int}[n] \rightarrow \{\texttt{int}[x] \mid \texttt{true}\}. \end{aligned}$$

Below we focus on the definition of the function $\texttt{range}$, and show how to derive $\mathcal {C}; \varGamma _1; \texttt{true}\vdash \texttt{if}\ n\ \texttt{then}\ {e_2}\ \texttt{else}\ {\texttt{Nil}()}: \texttt{ilistL}^![n]$ (which is required for deriving $\mathcal {C}\vdash D_1: \varGamma _0$), where

$$\begin{aligned} \varGamma _1 ={}&(\varGamma _0, n: \texttt{int}) \\ e_2 ={}&(\texttt{let}\ r=\texttt{range}(n - 1)\ \texttt{in}\ {\texttt{Cons}(n, r)}) \\ \texttt{ilistL}={}&\texttt{ilist}\langle {1;(\lambda ().\texttt{true}, \lambda ().0), (\lambda (x,y).\texttt{true}, \lambda (x,y).y+1)}\rangle . \end{aligned}$$

First, the type of $\texttt{range}(n - 1)$ in the body is derived as follows.

Second, the expression $\texttt{Cons}(n, r)$ is typed as:

where $\varGamma _2 = (\varGamma _1, r: \texttt{ilistL}[q])$ and $\varphi _2 = (n \ne 0 \wedge q = n - 1)$. Finally, using the judgments above, we obtain:

   $\square$

Our type system can also deal with properties on trees, as demonstrated in the following example.

Example 5

Recall the program $D_3$ given in Example 3. It is typed as $\mathcal {C}\vdash D_3: \varGamma _0$, where $\varGamma _0$ is:

$$\begin{aligned} \varGamma _0 ={} \{&\mathtt {gen\_tree}\!: \texttt{int}[n] \rightarrow \texttt{itreeZ}^![n], \\&\texttt{size}\!: \texttt{itreeZ}[n] \rightarrow \texttt{int}^![n], \\&\texttt{main}\!: \texttt{int}[n] \rightarrow \{\texttt{int}[x] \mid \texttt{true}\} \}. \end{aligned}$$

Here, $\texttt{itreeZ}= \texttt{itree}\langle 1;(\lambda ().\texttt{true},\lambda ().0), (\lambda (x,y_1,y_2).\texttt{true}, \lambda (x,y_1,y_2).y_1+y_2+1) \rangle$. Intuitively, $\texttt{itreeZ}[n]$ is the type of trees with n nodes. The expression $\texttt{Node}(*, \ell , r)$ in the definition of the function $\mathtt {gen\_tree}$ is typed by:

where

$$\begin{aligned} \varGamma _1 ={}&(\varGamma _0, n: \texttt{int}, m: \texttt{int}, \ell : \texttt{itreeZ}[m], r: \texttt{itreeZ}[n - 1 - m]) \\ \varphi _1 ={}&(n \ne 0). \end{aligned}$$

The last premise ($\models \varphi _1 \wedge y_1 = m \wedge y_2 = n - 1 - m \wedge z = y_1+y_2+1 \Rightarrow z = n$) uses the function $\lambda (x,y_1,y_2).y_1+y_2+1$ in $\texttt{itreeZ}$ to obtain an accumulated value for the tree size.

The $\texttt{match}$ expression in function $\texttt{size}$ is typed by:

where

$$\begin{aligned} \varGamma _2 ={}&(\varGamma _0, t: \texttt{itreeZ}[n]) \\ \varGamma _2' ={}&(\varGamma _2, \_: \texttt{int}, \ell : \texttt{itreeZ}[y_1], r: \texttt{itreeZ}[y_2]) \\ e_2 ={}&(\texttt{match}\ {t}\ \texttt{with}\ \{ \texttt{Leaf}() \rightarrow 0, \texttt{Node}(\_, \ell , r) \rightarrow e_3 \}) \\ e_3 ={}&1 + \texttt{size}(\ell ) + \texttt{size}(r) \\ \varphi _1' ={}&(n = 0) \\ \varphi _2' ={}&(n = 1 + y_1 + y_2). \end{aligned}$$

   $\square$

Remark 2

It is sometimes too restrictive to fix the $\beta$-part in rule T-Sub. For example, the function $\texttt{isort}$ of the program $D_2$ (defined in Example 2) is equivalent to the function $\texttt{isort}'$ defined below, which is obtained by substituting $\texttt{Nil}()$ in the match body of $D_2$ with l.

However, since l is returned directly, the argument and return types of $\texttt{isort}^\prime$ share the same $\beta$-part. Therefore, our type system cannot express that $\texttt{isort}^\prime$ converts an unsorted list to a sorted one. To relax the restriction, we need a more sophisticated version of the subtyping rule T-Sub, which would cause too much burden for the type inference procedure discussed in the next section. It is left for future work to overcome the problem above without incurring too much overhead for type inference.    $\square$

The following proposition states the soundness of the type system (recall the definition of safety in Sect. 2.3).

Proposition 1 (soundness)

Suppose $\mathcal {C}\vdash D:\varGamma$, with $\varGamma (\texttt{main})=\{(\beta _1,\ldots ,\beta _k)\mid \texttt{true}\}\rightarrow \{\beta \mid \texttt{true}\}$. Then, the program $D$ is safe.

The proposition follows from the soundness of a standard refinement type system without parameterization $\langle {n;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle$, as follows. Because only constructors are polymorphic on the part $\langle {n;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle$, if a program $D$ is well-typed, then by annotating each occurrence of constructor $L_i$ with the parameter $\langle {n;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle$, and treating the annotated constructor $L_i^{(\langle {n;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle )}$ as a new constructor, and the $\delta$-part $\texttt{d}\langle {n;(P_1,F_1),\ldots ,(P_k,F_k)}\rangle$ as the name of a new datatype, we can obtain a program $D'$ that is well-typed without the parameterization. The safety of $D'$ follows from the soundness of a standard refinement type system (without parameterization); hence $D$ is also safe.

Note that the completeness does not hold: there exists a program that is safe but not typable in our refinement type system. Beside the issue discussed in Remark 2, the sources of incompleteness include the restriction of the parameters of data types to integers. For example, consider the property of the append function: “a function takes two lists and returns the list obtained by appending two lists.” In theory, it is possible to encode all the information of a list by using Gödel encoding, but that is not possible in practice, where we have to restrict the underlying integer arithmetic, e.g., to linear integer arithmetic.

Fig. 4.

The flow of type inference

4 Inferring Parameterized Refinement Types

This section describes a type inference procedure, which takes a program (without type annotations) and a constructor type environment as input, and checks whether the program is well-typed. The overall flow of the type inference procedure is shown in Fig. 4.

In Step 1, we first determine the raw type of each expression, with the values of the part $[n;\widetilde{(P,F)}]$ kept unknown. For example, given the program $D_2$ in Example 2, we infer:

$$\begin{aligned} \texttt{gen}\mathbin {:}\texttt{int}\rightarrow \texttt{ilist}[\rho _1], \texttt{isort}: \texttt{ilist}[\rho _1]\rightarrow \texttt{ilist}[\rho _2], \end{aligned}$$

where $\rho _1$ and $\rho _2$ are variables representing the part $[n;\widetilde{(P,F)}]$. (Note that the same variable $\rho _1$ is assigned to the return type of $\texttt{gen}$ and the argument type of $\texttt{isort}$, since the return value of $\texttt{gen}$ is passed to $\texttt{isort}$.) This is performed by using an ordinary unification-based type inference algorithm.

In Step 2, the part $n$ and $\widetilde{F}$ of each raw type variable $\rho _i$ is chosen, while the predicates $\widetilde{P}$ are kept unknown. In Step 3, we prepare predicate variables for the unknown predicates in raw types and refinement predicates, and reduce the typability problem to the satisfiability problem for constrained Horn clauses (CHCs) [1]. We then invoke an off-the-shelf CHC solver [2, 4, 7] to check whether the obtained CHCs are satisfiable. If so, we can conclude that the program is well-typed (and outputs inferred types); otherwise, we go back to Step 2 and refine the $F$-part of raw types, with an increased value of $n$.

In the rest of this section, we explain more details of Steps 2 and 3.

4.1 Step 2: Instantiation of Raw Types with $\widetilde{F}$

In Step 2, we determine the components n and $\widetilde{F}$ of $\delta$.

For the sake of simplicity, the number of integer parameters n is shared by all types, and the functions $\widetilde{F}$ do not depend on $\delta$ but on $\texttt{d}$. On the other hand, the predicate variables $\widetilde{P}$ are specific to $\delta$. Thus, we explicitly write $\delta = \texttt{d}\langle {n;(P_{\delta ,1},F_{\texttt{d},1}),\ldots ,(P_{\delta ,k},F_{\texttt{d},k})}\rangle$ here.

We choose $n$ and $F_{\texttt{d},j}$ as follows, to ensure that the precision of type inference is monotonically improved at each iteration. Suppose $\mathcal {C}_\texttt{d}= \{L_1\mathbin {:}(\texttt{int}^{\ell _1}, \texttt{d}^{m_1})\rightarrow \texttt{d}, \ldots , L_k\mathbin {:}(\texttt{int}^{\ell _k}, \texttt{d}^{m_k})\rightarrow \texttt{d}\}$. Let us write $n^{(i)}$ and $F_{\texttt{d},j}^{(i)}$ for the values of $n$ and $F_{\texttt{d},j}$ at the $i$-th iteration of the refinement loop in Fig. 4. At the ($i+1$)-th iteration, we pick $n'>0$ and a tuple of functions $(F'_1,\ldots ,F'_k)$ with $F'_j\in \texttt{int}^{\ell _j+m_j n'}\rightarrow \texttt{int}^{n'}$ (that has not been chosen before) and set $n^{(i+1)}$ and $F^{(i+1)}_{\texttt{d},j}$ as follows.

$$\begin{aligned}&n^{(i+1)} := n^{(i)}+n'\\&F^{(i+1)}_{\texttt{d},j} := \lambda (\widetilde{x},\widetilde{y}_1,\ldots ,\widetilde{y}_{m_j}). (F^{(i)}(\widetilde{x}, \widetilde{y}'_1,\ldots ,\widetilde{y}'_{m_j}), F'_j(\widetilde{x}, \widetilde{y}''_1,\ldots ,\widetilde{y}''_{m_j})). \end{aligned}$$

Here, $\widetilde{x}$ and $\widetilde{y}_j$ are sequences of variables of length $\ell _k$ and $n^{(i+1)}$ respectively, and $\widetilde{y}_j = \widetilde{y}'_j, \widetilde{y}''_j$ with $|\widetilde{y'}_j|=n^{(i)}$ and $|\widetilde{y}''_i|=n'$. For example, if $n^{(i)}=1$ and $F_j^{(i)}(x, y_1,y_2)=x+y_1+y_2$ with $n'=1$ and $F_j'(x,y_1,y_2)=1+\max (y_1,y_2)$, then $F_j^{(i+1)}(x,y_{11},y_{12},y_{21},y_{22}) = (x+y_{11}+y_{21}, 1+\max (y_{12},y_{22}))$.

Since the choice of $n^{(i)}$ and $F^{(i)}_{\texttt{d},j}$ above ensures that the information carried by types monotonically increases, we can guarantee that our type inference procedure is relatively complete with respect to the (hypothetical³) completeness of the CHC solver used in Step 3, in the following sense. Let us assume that the language for describing functions of type $\bigcup _{j = 1}^\omega \texttt{int}^{l_i + m_i j} \rightarrow \texttt{int}^j$ is recursively enumerable; for example, we can restrict functions to those expressible in linear integer arithmetic. Then we can enumerate all the tuples of functions and use the $i$-th tuple as $(F_1',\ldots ,F_k')$ above. Suppose that a program $D$ is typable by using, as $F_{\texttt{d},j}$, functions belonging to the language assumed above. Then, assuming that the CHC solver used in Step 3 below is complete, our procedure eventually terminates and outputs “Verified”. (In other words, our procedure eventually terminates output “Verified”, or gets stuck in Step 3 due to the incompleteness of the CHC solver.) This is because the functions required for typing $D$ is eventually chosen and added to $F^{(i)}_{\texttt{d},j}$.

For the sake of efficiency, the actual implementation imposes a further restriction on the function $F'_j$ added at each iteration, at the sacrifice of relative completeness; see Sect. 5.1.

Remark 3

While we currently employ the same n for all data types, it can be effective to selectively add a parameter to an individual raw type, based on the unsatisfiable core returned from the solver in Step 3.

4.2 Step 3: Reduction to CHC Solving

In this step, we prepare predicate variables for the $P$-part of raw types and unknown refinement predicates $\varphi$, and construct a template of a type derivation tree. We then extract constraints on the predicate variables based on the typing rules. The extracted constraints consists of constrained Horn clauses (CHCs), of the following form:

$$ \forall \widetilde{x}.(H\Leftarrow B_1\wedge \cdots \wedge B_k), $$

where $B_i$ and $H$ are atomic constraints of the form $p(s_1,\ldots ,s_\ell )$ or integer constraints ($s_1\le s_2$, $s_1=s_2$,...). The program is well-typed (with the choice of $n$ and $\widetilde{F}$ in the previous step), just if the CHCs are satisfiable, i.e., if there exists an assignment of predicates to predicate variables that make all the clauses valid. The latter problem (of CHC satisfiability) is undecidable in general, but there are various efficient solvers that work well for many inputs [2, 4, 7].

Since the reduction from refinement type inference to the CHC satisfiability problem is fairly standard (see, e.g., [2, 18]), we sketch the reduction only informally, through an example.

Example 6

Let us recall the program $D_1$ in Example 1, and focus on the function $\texttt{range}$. When $n = 1$, we need to derive $\mathcal {C}; \varGamma _1; p_1(h) \vdash \texttt{if}\ h\ \texttt{then}\ {e_2}\ \texttt{else}\ {\texttt{Nil}()}: \tau _0$ (which is required in T-Prog for proving $\mathcal {C}\vdash D_1: \varGamma _0$), where

• $\varGamma _0 = (\texttt{range}\!: \{\texttt{int}[h] \mid p_1(h)\} \rightarrow \{\texttt{ilistL}[i] \mid p_2(h,i)\}, \ldots )$,

• $\varGamma _1 = (\varGamma _0, h: \texttt{int})$,

• $e_2 = (\texttt{let}\ r=\texttt{range}(h - 1)\ \texttt{in}\ {\texttt{Cons}(h, r)})$,

• $\tau _0 = \{\texttt{ilist}_1[i] \mid p_2(h,i)\}$, and

• $\texttt{ilist}_1 := \texttt{ilist}\langle {1;(p_3, \lambda ().0), (p_4, \lambda (x,y).y+1)}\rangle$.

The derivation for the judgment is of the form:

where $\varphi _2 = (p_1(h) \wedge h \ne 0 \wedge p_5(h,j))$ and $\tau _3 = \{\texttt{ilistL}[j] \mid p_5(h,j)\}$. From the side conditions of the subderivation on the righthand side, the following CHCs are obtained:

$$\begin{aligned} p_3()&{}\Leftarrow p_1(h) \wedge h = 0, \\ p_2(h,i)&{}\Leftarrow p_1(h) \wedge h = 0 \wedge i = 0. \end{aligned}$$

CHCs are also obtained from the other subderivation in a similar manner.    $\square$

5 Implementation and Experiments

This section reports an implementation and experimental results.

5.1 Implementation

We have implemented a prototype program verifier for a subset of OCaml, which supports first-order functions, integers, and recursive data structures, based on the type inference procedure described above. As the backend CHC solvers, we employed multiple solvers: Z3 [12] ver. 4.8.12, HoIce [2] ver. 1.9.0, and Eldarica [4] ver. 2.0.7; that is because these solvers have pros and cons, and their running times vary depending on problem instances, as we report in Sect. 5.2.

As for the function $F'$ in Sect. 4.1, the current implementation supports only the following functions $f_{i,\diamond }\in \texttt{int}^{\ell _k+m_k}\rightarrow \texttt{int}$ with $i\in \{1,2,3\}$ and $\diamond \in \{+,\max ,\min \}$ (where $n'$ in Sect. 4.1 is set to $1$).

$$\begin{aligned}&f_{1,\diamond }(x_1,\ldots ,x_{\ell _k},y_1,\ldots ,y_{m_k}) = \left\{ \begin{array}{ll} 1+(y_1\diamond \cdots \diamond y_{m_k}) &{} \text{ if } m_k>0\\ 0 &{} \text{ otherwise } \end{array}\right. \\&f_{2,\diamond }(x_1,\ldots ,x_{\ell _k},y_1,\ldots ,y_{m_k}) = x_1\diamond \cdots \diamond x_{\ell _k} \diamond y_1\diamond \cdots \diamond y_{m_k}\\&f_{3,\diamond }(x_1,\ldots ,x_{\ell _k},y_1,\ldots ,y_{m_k}) = x_1\diamond \cdots \diamond x_{\ell _k}, \end{aligned}$$

and chooses $f_{1,+},f_{2,+},f_{3,+},f_{1,\max },f_{2,\max },f_{3,\max },f_{1,\min },f_{2,\min },f_{3,\min }$ in this order, at each iteration. (Here, $\max$ and $\min$ are operations over integers extended with $-\infty$ and $\infty$.) In the case of lists, $f_{1,+}$, $f_{2,+}$, $f_{3,+}$, $f_{2,\max }$, and $f_{2,\min }$ can be used for computing the length, the sum of elements, the head element, the maximal element, and the minimal element of a list, respectively; since $f_{1,\max }$ and $f_{1,\min }$ coincide with $f_{1,+}$ for lists, it will be excluded out. Since the set of functions added as $F'$ is finite, the current implementation obviously does not satisfy the relative completeness discussed in Sect. 4.1. Supporting more functions is not difficult in theory, but because the current implementation seemed to have already hit a certain limitation of the state-of-the-art CHC solvers (as reported in the next subsection), we plan to add more functions only after more efficient CHC solvers become available.

5.2 Experiments and Results

To evaluate the effectiveness of our approach, we have tested our prototype tool for several list/tree-processing programs. The experiments were conducted on a machine with Ubuntu 20.04.1 on Windows Subsystem for Linux 2, AMD Ryzen 7 3700X 8-Core Processor, and 16GB RAM.

Table 1. The experimental results

Table 1 summarizes the experimental results. The benchmark set consists of the following programs.

• “list-sum” takes an integer $m$ as an input, randomly generates a list so that the sum of elements is $m$, and then checks that the sum of elements is indeed $m$. Similarly, “list-max” generates a list so that the maximum element is $m$, and checks that the maximum element is indeed $m$, and “list-sorted” randomly generates a sorted list and checks that the list is indeed sorted.

• “range-X” generates a list $[m;m-1;\cdots ;1]$ using the function $\texttt{range}$ in Example 1, and checks its properties, where the property is “$n=0$ if the generated list is null, and $m>0$ otherwise” for X=basic, “the length is $m$” for X=len. The program “range-concat-len” calls $\texttt{gen}(m)$ twice, concatenates the two lists, and check that the length of the resulting list is $2m$.

• “isort-X” takes an integer $m$ as an input, generates a list of length $m$, sorts it with $\texttt{isort}$ in Example 2, and checks properties of the resulting list, where the property is “the length of the list is $m$” for X=len, and “the list is sorted” for X=sorted.

• “msort-X” is a variation of “isort-X”, where $\texttt{isort}$ is replaced with a function for the merge sort.

• “tree-size” (“tree-depth”, resp.) takes an integer $m$ as an input, generates a tree of size (depth, resp.) $m$, and checks that the size (depth, resp.) of the tree is indeed $m$ (for X=size).

• “bst-X” generates a binary search tree of a given size, and checks that the tree has the expected size (for X=size) or that the tree is a valid binary search tree (for X=sorted).

Appendix A shows some of the concrete programs used in the experiments.

In the table, the column “#Lines” shows the number of lines of the program (excluding empty and comment lines), and the column “n” shows the final value of $n$ in Fig. 4, when the verification succeeded; the cell filled with “—” indicates a timeout (due to the backend CHC solver), where the time limit was set to 300 s. The columns “Time” and “CHC solver” show the running time and the backend CHC solver. Actually, we have run our tool for each of the three CHC solvers: Z3 [12] ver. 4.8.12, HoIce [2] ver. 1.9.0, and Eldarica [4] ver. 2.0.7, and the table shows only the best result. The result for other solvers are reported in Appendix A. The columns “#clauses” and “#pvars” show the numbers of output clauses and predicate variables, respectively (which do not depend on the value of n).

The results show that our tool works reasonably well: we are not aware of fully automated tools that can verify most of those programs. Our tool failed, however, to verify “msort-len”, “msort-is-sorted”, and “bst-sorted”. To analyze the reason, we have manually prepared an optimal choice of functions $\widetilde{F}$ for those problems, and run the CHC solvers for the resulting CHC problems. None of the CHC solvers could solve the problems in time. This indicates that the main bottleneck in the current tool is not the choice of functions $\widetilde{F}$ discussed in Sects. 4.1 and 5.1, but rather the backend CHC solver. We expect that “msort-len”, “msort-is-sorted”, and “bst-sorted” can be automatically verified by our method if a more efficient CHC solver becomes available. It would be, however, important also to improve the heuristics for choosing n and $\widetilde{F}$, as briefly discussed in Remark 3.

6 Related Work

As already mentioned in Sect. 1, the idea of parameterizing recursive types with indices to represent various properties goes back at least to Xi and Pfenning’s work on dependent ML [23, 24]. In their system, however, explicit declarations of refinement types are required for data constructors and recursive functions. Kawaguchi et al. [5] introduced recursive refinement types, which allows a restricted form of parameterization of datatypes with predicates, and Vazou et al. [21] have introduced abstract refinement types, which are refinement types parameterized with predicates. Like Xi and Pfenning’s system (and unlike ours), those systems also require explicit declarations of abstract refinement types for datatype constructors and/or functions, although refinement parameters in the code part can be omitted and automatically inferred (cf. [21], Sect. 3.4). The type system of Vazou et al. [21] supports polymorphism on predicates, unlike our type system.

The reduction from (ordinary) refinement types to the CHC satisfiability problem has been well studied [2, 3, 19]; we used that technique in Step 3 of our type inference procedure. The problem of inferring parameterized recursive refinement types appears to be related with that of inferring implicit parameters in refinement type systems [17, 20]. In fact, Tondwalkar et al. [17] reduced the inference problem to the problem of solving existential CHCs, an extension of the CHC problem, and our problem of inferring $P$ and $F$ can also be reduced to that problem. We, however decided not to take that approach, because efficient solvers for existential CHCs are not available.⁴ We instead designed a heuristic procedure to construct $F$, and reduced the rest of the inference problem to the satisfiability problem for ordinary CHCs.

There have been other (non-type-based) approaches to verification of programs manipulating recursive data structures. The series of work on TVLA [10, 11] targets programs with destructive updates, and infers the shape of data structures by using a 3-valued logic. Besides the difference in the target programs, to our knowledge, their analysis fixes predicates used for abstraction a priori (e.g., in [10], “instrumentation predicates” are specified by a user of the tool), whereas our tool fixes only the set of functions $F_j$’s for mapping data structures to integers, and leaves it to the underlying CHC solver to find appropriate predicates. Thanks to the type-based approach, our approach can also be naturally extended to deal with higher-order programs.

7 Conclusion

We have introduced parameterized recursive refinement types (PRRT) that can express various properties of recursive data structures in a uniform manner, and proposed a type inference procedure for PRRT, to enable fully automatic verification of functional programs that use recursive data structures. We have implemented a prototype automated verification tool, and confirmed that the tool can automatically verify small but non-trivial programs. Future work includes an extension of the verification tool for a full-scale functional language, and a further refinement of the type inference procedure to improve the efficiency of the tool.

Appendices

Appendix

A Details of Experiments

Table 2 presents the experimental results for each backend CHC solver. The columns “n” and “Time” for each solver have the same meaning as Sect. 5.2.

Table 2. The results of verification with three solvers

As examples of the benchmark programs, Listings 1.1 and 1.2 respectively show the programs named “list-sum” and “bst-size” in Sect. 5.2.