2.1 The Dijkstra Monad Approach

As mentioned already, Swamy et al. [15] introduced a semi-automated verification method targeting higher-order programs with monadic effects, based on a monad of predicate transformers called the Dijkstra monad. The types of effectful computations has the form \(\texttt{D}\; t\; w\), where \(\texttt{D}\) is the Dijkstra monad defined for each kind of effect, \(t\) is the pure type of the result, and \(w\) is a predicate transformer that describes the behavior of the computation by mapping postconditions to preconditions.

For example, consider the following program, which manipulates a state of type \(\texttt {int}\).

Dummy

The function \(\texttt{increment}\) gets the current state \(x\) and writes back \(x+1\), thus incrementing the state. The function is given the type:

$$\begin{aligned} \texttt {unit}\rightarrow \mathtt {D^{STATE}}\;{\texttt {unit}}\;{(\lambda s_\text {init}, post.\ post\, \texttt {()}\, (s_\text {init} + 1))}. \end{aligned}$$

The predicate transformer \(\lambda s_\text {init}, post.\ post\, \texttt {()}\, (s_\text {init} + 1)\) has the type \(\texttt {int}\rightarrow (\texttt {unit}\rightarrow \texttt {int}\rightarrow \texttt {prop}) \rightarrow \texttt {prop}\). The first parameter \(s_\text {init}\) stands for the initial state, and the second parameter \(post\) is the postcondition, which is a binary predicate on the result value and the final state. Given the parameters, the predicate transformer returns a precondition that guarantees the postcondition to hold after the computation. For example, to prove that the final state is positive after calling \(\texttt{increment}\), it suffices to apply the predicate transformer to the postcondition \(\lambda \texttt {()}. \lambda s_\text {final}.\ s_\text {final}>0\), and prove that the computed precondition \( s_\text {init}+1>0 \) holds before the call.

To derive a predicate transformer from a program, Swamy et al. [15] proposed a kind of a dependent type system and an inference algorithm. For programs without recursion, predicate transformers and the associated verification conditions can automatically be inferred, although users may optionally provide type annotations to specify the behavior of sub-expressions. For recursive functions, however, those annotations must be provided, as in other deductive (verification-condition-generation) approaches to program verification.

2.2 The HFL(Z) Approach

Kobayashi et al. [9, 17] proposed an approach to higher-order program verification based on HFL(Z), an extension of Viswanathan and Viswanathan’s higher-order fixpoint logic [16] with integers. In that approach, a higher-order functional program with a regular-temporal-property specification is automatically translated into a formula of HFL(Z), so that the program satisfies the property just if the formula is valid. The validity of the formula is undecidable in general, but automated (but inevitably incomplete due to the undecidability) validity checkers for HFL(Z) have been implemented since then [5, 6, 8]; the approach thus realizes fully automated verification of higher-order programs.

By using fixpoint operators, the properties of recursive functions can be precisely expressed in the HFL(Z) approach, without any need for manual annotations. For example, consider the following function.

Dummy

The function \(\texttt{sum}\) computes the sum of the first \(n\) natural numbers if \(n\) is a non-negative integer, and diverges otherwise. If we are interested in the total correctness, it suffices to translate the function to the predicate \(\textsf{Sum}\) defined by the following fixpoint equation:

$$ \textsf{Sum} =_\mu \lambda n.\ \lambda k.\ (n=0 \Rightarrow k\; 0) \wedge (n\ne 0 \Rightarrow \textsf{Sum}\; (n-1)\; (\lambda s.\ k\; (n+s))). $$

Here, the equation defines \(\textsf{Sum}\) as the least predicate that satisfies the equality. The above equation is automatically obtained from the function definition by applying the CPS transformation (note that \(k\) above represents a continuation), and by encoding the conditional expression into the corresponding logical formula. \(\textsf{Sum}\;n\) can be viewed as a predicate transformer; it takes a postcondition \(k\), and returns the corresponding precondition on \(n\) for \(\texttt{sum}\) to terminate and for the return value \(r\) to satisfy \(k\;r\). The total correctness is thus expressed as \(\forall n\ge 0.\textsf{Sum}\;n\;(\lambda r.r=n(n+1)/2)\). If we are interested in partial correctness instead, then we just need to replace \(=_\mu \) with \(=_\nu \) in the above fixpoint equation, so that \(\textsf{Sum}\) is defined as the greatest predicate that satisfies the equation.

The HFL(Z) approach targets a higher-order functional language with general recursion, nondeterminism, and an abstract notion of events, but various other effects (such as states and exceptions) can be encoded by a combination with standard transformations for functional programs such as store passing translation and variants of CPS transformations. For example, to deal with the increment function in Section 2.1, we first apply the store-passing transformation (and inline get and put) to obtain:

Dummy

We can then obtain the following HFL(Z) predicate \(\textsf{Inc}\) by using the CPS (and currying) transformation:

$$ \textsf{Inc} := \lambda \texttt {()}.\lambda s.\lambda k.k\,\texttt {()}\, (s+1). $$

Suppose we wish to prove that, given a non-negative initial state, the state after calling increment is positive. That is expressed by the formula \(\forall s\ge 0.\textsf{Inc}\,\texttt {()}\,s\,(\lambda \texttt {()}.\lambda s'.s'>0)\). Here, notice that \(\textsf{Inc}\,\texttt {()}=_\beta \lambda s.\lambda k.k\,\texttt {()}\, (s+1)\) matches the predicate transformer obtained in the DM approach in Section 2.1.

2.3 The Similarity between Dijkstra Monads and HFL(Z)

We have already seen similarities between the two approaches for first-order functions (succ in Section 1 and increment in this section). We discuss a higher-order case in this subsection. Let us consider the following twice function.

Dummy

In the DM approach, the function twice can be given the following type.

$$ \forall w_f. f\mathbin {:}(x:\texttt {int}\rightarrow \texttt{D}\;\texttt {int}\;(w_f\;x))\rightarrow x\mathbin {:}\texttt {int}\rightarrow \texttt{D}\;\texttt {int}\;(\lambda p.w_f\;x\;(\lambda y.w_f\;y\;p)). $$

Here, the type is polymorphic on the predicate transformer \(w_f\) for \(f\). Using \(w_f\), the precondition for the part \(f\,y\) (with respect to the postcondition \(p\)) is expressed as \(w_f\;y\;p\), and thus the predicate transformer for twice can be expressed as \(\lambda p.w_f\;x\;(\lambda y.w_f\;y\;p)\). Since succ has type \(x\mathbin {:}\texttt {int}\rightarrow \texttt{D}\;\texttt {int}\;(\lambda p.p(x+1))\), we obtain the type \( x\mathbin {:}\texttt {int}\rightarrow \texttt{D}\;\texttt {int}\;(\lambda p.w_\texttt{succ}\;x\;(\lambda y.w_\texttt{succ}\;y\;p)) \) for plustwo, where \(w_\texttt{succ}:=\lambda x.\lambda p.p(x+1)\). By reducing it, we obtain \( x\mathbin {:}\texttt {int}\rightarrow \texttt{D}\;\texttt {int}\;(\lambda p.p(x+2))\). In the HFL(Z) approach, the function twice is converted to the following predicate \(\textsf{Twice}\):

$$ \textsf{Twice} := \lambda f.\lambda x.\lambda k.f\;x\;(\lambda y.f\;y\;k). $$

The part \(\lambda k.f\;x\;(\lambda y.f\;y\;k)\) corresponds to \(\lambda p.w_f\;x\;(\lambda y.w_f\;y\;p)\) from the DM approach. The function plustwo is converted to \(\textsf{Twice}\;\textsf{Succ}\), which can be simplified as follows.

$$\begin{aligned} \textsf{Twice}\;\textsf{Succ} & = (\lambda f.\lambda x.\lambda k.f\;x\;\lambda y.f\;y\;k)(\lambda x.\lambda k.k(x+1)) =_\beta \lambda x.\lambda k.k(x+2). \end{aligned}$$

The part \(\lambda k.k(x+2)\) corresponds to \(\lambda p.p(x+2)\). Thus, there are some correspondences between the DM and HFL(Z) approaches even at higher-order.

Table 1 summarizes the correspondence between the two approaches we have seen so far (with some \(\alpha \)-renaming). As clear from the table, HFL(Z) formulas can actually be extracted from types of Dijkstra monads. In a higher-order case, HFL(Z) formulas correspond to polymorphic types on predicate transformers. A formal connection is established in the next section.

Dummy

3.1 Language

This subsection introduces a simple call-by-value, effectful higher-order functional language, which shall be used as the common language for formally comparing the two approaches.

We exclude recursion and restrict the shape of types; as discussed in Section 4, some important differences show up for recursion and certain types.

We introduce a type system to reject inappropriate expressions such as \(1+\texttt {()}\). We call this type system the simple (monadic) type system, to distinguish it from the type system for Dijkstra monads introduced later. The typing rules are given in Figure 1, which define two kinds of judgments \(\varGamma \mathrel {\vdash }e:s\) and \(\varGamma \mathrel {\vdash }e:\texttt{M}\; a\), where the latter is for effectful computations. In the rules and , \(\varGamma \mathrel {\vdash }\widetilde{e}:\widetilde{\texttt {int}}\) means \(\varGamma \mathrel {\vdash }e_i:\texttt {int}\) for every \(i\in \{1,\ldots ,k\}\). In the rule , \(t^{ act }\) denotes the type of the effect action \( act \) (which is introduced below).

We have so far parameterized the language by effects. A concrete language and its semantics are determined by the parameters given below, which we call effect parameters. The semantics of effect operations are given in the form of predicate transformers; we assume the simply-typed lambda calculus with \(a\) and \(\texttt {prop}\) (which is the type of propositions) as base types and also with appropriate constants (such as logical connectives \(\wedge , \vee : \texttt {prop}\rightarrow \texttt {prop}\rightarrow \texttt {prop}\), the predicate \(\texttt{pred}: \texttt {int}^k\rightarrow \texttt {prop}\) for each \(k\)-ary predicate \(\texttt{pred}\) in the source language, and the operator \(\texttt{op}:\texttt {int}^k\rightarrow \texttt {int}\) for each \(k\)-ary operator \(\texttt{op}\) in the source language) for describing predicate transformers.

In the field of the DM approach, the former three parameters are called a specification monad, and the latter three yield the DM type of effect actions. Methods to obtain these parameters in a correct-by-construction manner have been studied by Ahman et al. [1] and Maillard et al. [12]. According to Ahman et al.’s result, reinterpreted by Maillard et al., for effects that can be represented as monad transformers, these parameters can be obtained by applying the monad transformer to the continuation monad with \(\texttt {prop}\) as the answer type.

We give examples of effect parameters, some of which can be derived from monad transformers.

Given the effect parameters above, the semantics of the language can be given as a predicate transformer semantics. We omit the definition here, as the translation from programs to HFL(Z) formulas given in Section 3.3 can actually be viewed as the predicate transformer semantics (although the authors [9, 17] did not provide that observation).

3.2 The Dijkstra Monad Approach

The Dijkstra monad approach is formalized as another type system for the language, which we call the DM type system. We use \(\mathrel {\vdash ^\textrm{DM}}\) instead of \(\mathrel {\vdash }\) for a type judgment of the DM type system. The syntax of types is given below.

$$\begin{aligned} & a \text{(base } \text{ types) } :\,\!:= \texttt {unit}\mid \texttt {int}\\ & \pi \text{(predicate } \text{ transformer } \text{ types) } :\,\!:= a\mid \texttt {prop}\mid \pi \rightarrow \pi \qquad \\ & \tau \text{(function } \text{ types) } :\,\!:= x\mathbin {:} \varsigma \rightarrow \rho \mid \forall u\mathbin {:}\pi .\ \tau \\ & \varsigma \text{(argument } \text{ types) } :\,\!:= a\mid \tau \qquad \qquad \rho \text{(return } \text{ types) } :\,\!:= \texttt{D}\; a\; w\mid \tau \qquad \\ & w \text{(predicate } \text{ transformers) }:\,\!:= e \mid \texttt{pred}{(\widetilde{e})} \mid \lnot \texttt{pred}{(\widetilde{e})} \mid w_1 \wedge w_2 \mid w_1 \vee w_2 \qquad \\ &\qquad \qquad \qquad \qquad \qquad \mid \lambda u\mathbin {:}\pi .\ w\mid w_1 \;w_2 \mid {\texttt {if~}\texttt{pred}(\widetilde{e})\texttt {~then~}w_1\texttt {~else~}w_2} \end{aligned}$$

Compared with the simple monadic type system, we introduced the type \(\pi \) for predicate transformers, and changed the type of a monadic computation from \(\texttt{M}\; a\) to \(\texttt{D}\; a\; w\), where \(w\) is a predicate transformer of type \(\texttt{W}\;a\). The metavariable \(a\) is inherited from the simple type system, and the metavariables \(\tau , \varsigma \), and \(\rho \) correspond to \(t\), \(s\), and \(r\) respectively, in the simple monadic type system. Function types have been extended to dependent function types of the form \(x\mathbin {:} a_1 \rightarrow \texttt{D}\; a_2\; w\), etc., so that \(x\) may occur in the predicate transformer \(w\). We also allow polymorphic types \(\forall u\mathbin {:}\pi .\ \tau \) on predicate transformers \(u\). The language of predicate transformers, ranged over by \(w\), is defined by extending the expression syntax with constructs of predicate logic, \(\lambda \)-abstractions and applications of the type \(\pi \), and (non-monadic) conditional expressions; we assume that the language of predicate transformers subsumes the simply-typed \(\lambda \)-calculus assumed in Section 3.1 for describing predicate transformers. We may omit type annotations for predicate transformer variables and just write \(\lambda u.\ w\) and \(\forall u.\ \tau \) for \(\lambda u\mathbin {:}\pi .\ w\) and \(\forall u\mathbin {:}\pi .\ \tau \) when they are clear from the context. Note that this definition is a fragment of the original type system of Dijkstra monads [15]: for example, refinement types and polymorphism are excluded.

The typing rules of the DM type system for expressions and predicate transformers are shown in Figures 2 and 3, respectively. In the rule , \(\varsigma ^{\textrm{toM}}\) denotes the simple monadic type obtained by erasing predicate transformers, as defined by:

$$\begin{aligned} & a^{\textrm{toM}} :=a\quad (\texttt{D}\; a\; w)^{\textrm{toM}}=\texttt{M}\; a \quad \\ & (x\mathbin {:}\varsigma \rightarrow \rho )^{\textrm{toM}} :=\varsigma ^{\textrm{toM}}\rightarrow \rho ^{\textrm{toM}} \quad (\forall u\mathbin {:}\pi . \tau )^{\textrm{toM}} :=\tau ^{\textrm{toM}}. \end{aligned}$$

The rules DM-Ret and DM-LetIn reveal that the Dijkstra monad \(\texttt{D}\; a\; w\) is a monad indexed by the monad \(\texttt{W}\) of predicate transformers. The monadic operators \(\mathtt {return^{W}}\) and \(\mathtt {bind^{W}}\) of \(\texttt{W}\) are used in the typing rules of return expressions and let-in expressions, respectively. When a pure expression is lifted to an effectful computation using the return expression, it is injected into the predicate transformer using \(\mathtt {return^{W}}\). The predicate transformer of a let-expression is computed by composing the two predicate transformers of its two sub-expressions using \(\mathtt {bind^{W}}\).

In addition to typing rules guided by the expression syntax, we have rules , , and for conversion and introduction/elimination of universal quantifiers. The original type system of Dijkstra monads [15] has a subsumption rule, but we introduced the conversion rule instead for simplicity. The equivalence relation \(\varGamma \mathrel {\vdash ^\textrm{DM}}\varsigma =_{\beta \eta }\varsigma '\) is defined based on the \(\beta \eta \)-equality of predicate transformers inductively on the structure of types, where the base case \(\varGamma \mathrel {\vdash ^\textrm{DM}}\texttt{D}\; a\; w_1 =_{\beta \eta } \texttt{D}\; a\; w_2\) holds just if \(w_1 =_{\beta \eta } w_2\). The type of an action \(\texttt{call}^{ act }\) is constructed from the simple type \(t^{ act }\) and the predicate transformer \(w^{ act }\), using the transformation \(\operatorname {toDM}[r, w]\), proposed by Ahman et al. [1]. Intuitively, this transformation yields a DM type of an expression of type \(r\) whose behavior is specified by the predicate transformer \(w\). It is defined as follows.

$$\begin{aligned} &\operatorname {toDM}[\texttt{M}\; a, w] := \texttt{D}\; a\; w \\ &\operatorname {toDM}[a\rightarrow r, w] := x: a\rightarrow \operatorname {toDM}[r, w\ x] \\ &\operatorname {toDM}[t\rightarrow r, w] := \forall w_{x}: {t}^{\textrm{WP}}.\ x: \operatorname {toDM}[t, w_{x}] \rightarrow \operatorname {toDM}[r, w\ w_{x}] \quad (x, w_{x} \text {: fresh}). \end{aligned}$$

As we see in the third line, when \(r\) is an arrow type taking a function as the parameter \(x\), we universally quantify over the predicate transformer \(w_{x}\) of the function. The type of \(w_{x}\) is calculated from the simple type \(r\), defined below:

$$\begin{aligned} & {a}^{\textrm{WP}} := a\qquad {(\texttt{M}\; a)}^{\textrm{WP}} := {\texttt{W}\;a} \qquad {(s\rightarrow r)}^{\textrm{WP}} := {s}^{\textrm{WP}} \rightarrow {r}^{\textrm{WP}} \end{aligned}$$

Essentially, the translation replaces the monadic type \(\texttt{M}\; a\) with the type \(\texttt{W}\;a\). Note that the transformations \(\operatorname {toDM}[r, w]\) and \({r}^{\textrm{WP}}\) are called elaboration and the \(\star \)-transformation, respectively, by Ahman et al. [1]. Below we demonstrate how the DM type of \(\texttt{call}^{put}\) is calculated. Recall the definitions \(t^{put}=\texttt {int}\rightarrow \texttt{M}\; \texttt {unit}\) and \(w^{put}=\lambda x.\lambda h.\lambda p. p\,\texttt {()}\,x\) from Example 2.

$$\begin{aligned} \operatorname {toDM}[t^{put}, w^{put}] &=\operatorname {toDM}[\texttt {int}\rightarrow \texttt{M}\; \texttt {unit}, \lambda x.\lambda h.\lambda p. p\,\texttt {()}\,x] \\ &=x:\texttt {int}\rightarrow \texttt{D}\; \texttt {unit}\; ((\lambda x.\lambda h.\lambda p. p\,\texttt {()}\,x)\;x) \\ &=_\beta x:\texttt {int}\rightarrow \texttt{D}\; \texttt {unit}\; (\lambda h.\lambda p. p\,\texttt {()}\,x) \end{aligned}$$

A higher-order example of the calculation \(\operatorname {toDM}[t, w]\) is given later in Section 3.4. Note that the DM type \(\operatorname {toDM}[r, w]\) is consistent with the simple type \(r\), that is, \((\operatorname {toDM}[r, w])^{\textrm{toM}}=r\).

Example 3

Let us consider the following expression, which is equivalent to the function twice discussed in 2.3.

$$\begin{aligned} \lambda f: (\texttt {int}\rightarrow \texttt{M}\; \texttt {int}). \lambda x:\texttt {int}. \texttt {let~}y=f\;x\texttt {~in~}f\;y. \end{aligned}$$

This expression is typed as follows:

Dummy

Here, \(\varGamma := w_{f}:\pi _{w_{f}}, f:\tau _f,x:\texttt {int}\), where:

$$\begin{aligned} &\pi _{w_{f}}:= \texttt {int}\rightarrow \texttt{W}\;\texttt {int} & \tau _f:= z:\texttt {int}\rightarrow \texttt{D}\; \texttt {int}\; (w_{f}\;z)\\ &w_\texttt{twice}:= \mathtt {bind^{W}}\;(w_{f}\;x)\;(\lambda y. w_{f}\;y) & e_\texttt{twice}:= \texttt {let~}y=f\;x\texttt {~in~}f\;y\\ \end{aligned}$$

3.3 The HFL(Z) Approach

This subsection formalizes a translation from a program to a HFL(Z) formula, which represents the predicate transformer of the program. HFL(Z) is a higher-order logic with least/greatest fixpoints and integers, introduced by Kobayashi et al. [9] as an extension of higher-order modal fixpoint logic [16].

HFL(Z) [9] has an associated simple type system to exclude ill-formed formulas. The type system is essentially that of the simply-typed \(\lambda \)-calculus with operators, constant predicates, and logical connectives. A concrete definition of the type system is deferred to the longer version [19]. We assume that HFL(Z) contains, as a sublanguage, the simply-typed \(\lambda \)-calculus assumed in Section 3.1 for describing predicate transformers.

Reduction from Program Verification In this section, we introduce the translation from programs to HFL(Z) formulas.

3.4 Formalization of the Correspondence

Now we are ready to formalize the correspondence between the two approaches. We first show that there is a type derivation in the Dijkstra monad approach corresponding to the program transformation of the HFL(Z) approach.

The type system of the Dijkstra monad approach allows freedom in the choice of types of function parameters and the use of conversion and quantification rules. For example, \(\lambda f: (\texttt {int}\rightarrow \texttt{M}\; \texttt {int}).\ \lambda x:\texttt {int}.\ f\;(x+1)\), which has type \((\texttt {int}\rightarrow \texttt{M}\; \texttt {int})\rightarrow \texttt {int}\rightarrow \texttt{M}\; \texttt {int}\) in the simple monadic type system, can be given any of the following types in the DM type system:

Dummy

The first type abstracts over the predicate transformer of \(f\), while the second and third types accept only function arguments having a specific predicate transformer. For example, a function of the first type can be applied to both \(\lambda y. \texttt {return}\ (y+10)\) and \(\lambda y. \texttt {return}\ y\), but a function of the second type can be applied to \(\lambda y. \texttt {return}\ (y+10)\) but not to \(\lambda y. \texttt {return}\ y\), and a function of the third type can be applied to \(\lambda x. \texttt {return}\ y\) but not to \(\lambda y. \texttt {return}\ (y+10)\). Since the output of the transformation by the HFL(Z) approach is \(\lambda f.\ \lambda x.\ f(x+1)\), deriving the first type

$$\begin{aligned} \forall w_{f}.\ f:(y\mathbin {:}\texttt {int}\rightarrow \texttt{D}\; \texttt {int}\; (w_{f}\;y)) \rightarrow x:\texttt {int}\rightarrow \texttt{D}\; \texttt {int}\; (w_{f}(x+1)) \end{aligned}$$

is the most natural choice in order to show the correspondence. Actually, this type is obtained as \(\operatorname {toDM}[(\texttt {int}\rightarrow \texttt{M}\; \texttt {int})\rightarrow \texttt {int}\rightarrow \texttt{M}\; \texttt {int}, \lambda f. \lambda x.\ f(x+1)]\), as confirmed by the following calculation.

$$\begin{aligned} &\operatorname {toDM}[(\texttt {int}\rightarrow \texttt{M}\; \texttt {int})\rightarrow \texttt {int}\rightarrow \texttt{M}\; \texttt {int}, \lambda f. \lambda x.\ f(x+1)]\\ =& \forall w_{f}. f\mathbin {:}\operatorname {toDM}[\texttt {int}\rightarrow \texttt{M}\; \texttt {int}, w_{f}]\rightarrow \operatorname {toDM}[\texttt {int}\rightarrow \texttt{M}\; \texttt {int}, (\lambda f. \lambda x.\ f(x+1))w_{f}]\\ =&\cdots \\ =& \forall w_{f}. f:(y\mathbin {:}\texttt {int}\rightarrow \texttt{D}\; \texttt {int}\; (w_{f}\;y)) \rightarrow x:\texttt {int}\rightarrow \texttt{D}\; \texttt {int}\; (w_{f}(x+1)). \end{aligned}$$

Here, we have omitted the type of \(w_{f}\). Actually, this observation can be generalized: when the parameter \(f\) has the simple type \(t\), we choose \(\operatorname {toDM}[t, w_{f}]\) as the DM type for \(f\), where \(w_{f}\) is universally quantified. Hereafter, we call \(\operatorname {toDM}[t, w_{f}]\) as the canonical DM type corresponding to the simple type \(t\) specified by the predicate transformer \(w_{f}\).

To deal with open terms, we also need to rename variables. This is due to the observation that the DM type abstracts over the behavior of functional parameters using universal quantification of its predicate transformer, while the result of the transformation \({(\cdot )}^\textrm{DMWP}\) takes the translated higher-order predicate as an argument. For example, the function \(\lambda f: (\texttt {int}\rightarrow \texttt{M}\; \texttt {int}).\ f\;0\) can be given the type while the program transformation yields . As indicated by the red color, in actually corresponds to in the DM type, rather than \(f\). Based on this observation, we rename \(f\) to \(w_{f}\), by using the substitution \(\sigma _\varGamma \), defined by: \(\sigma _\varGamma (x) = w_{x}\) if \(\varGamma (x)\) contains \(\texttt{M}\) and \(\sigma _\varGamma (x) = x\) otherwise.

Now, the correspondence between the typing rules of DM and the program transformation \({(\cdot )}^\textrm{DMWP}\) on open terms can be stated as the following lemma.

The proof is found in the longer version [19]. As a special case of the lemma above, when the type environment \(\varGamma \) is empty, we have \(\,\mathrel {\vdash ^\textrm{DM}}e: \operatorname {toDM}[r, w] \) for \(w= {e}^\textrm{DMWP}\), confirming that \(w={e}^\textrm{DMWP}\) indeed serves as a witness for the condition \(\,\mathrel {\vdash ^\textrm{DM}}e: \operatorname {toDM}[r, w] \) of Theorem 1.

It remains to show \(w={e}^\textrm{DMWP}\) also satisfies \({w}^\dagger = {e}^{\textrm{HFL}}\), the second condition of Theorem 1, as stated in the following lemma.

We now obtain Theorem 1 as a corollary of the two lemmas above.

We now show the converse, i.e., that for every predicate transformer derived in the DM approach, an at least equally good predicate transformer can be obtained in the HFL(Z) approach. We assume that the DM type system is sound with respect to the predicate transformer semantics (as defined in Section 3.3 by the transformation to HFL(Z) formulas), i.e., if \(\mathrel {\vdash ^\textrm{DM}}e: \texttt{D}\; a\; w\) holds, then \(w\) is a sound predicate transformer (even though it may not be the weakest one). Then the following theorem follows immediately from the assumption.

4.1 On Nested Monads

To see the difference between the two approaches in the presence of nested monads, let us consider the following program:

Dummy

Here, increment is as defined in Section 2. In the DM approach, the function nest is given the type \(\texttt {unit}\rightarrow \texttt{D}^{\texttt{STATE}}\; (\texttt {unit}\rightarrow \texttt{D}^{\texttt{STATE}}\;\texttt {unit}\;w_2)\;w_1\) where \(w_1=\lambda h. \lambda p.p\,\texttt {increment}\, (h+2)\) and \(w_2=\lambda h. \lambda p.p\,\texttt {()}\,(h+1)\). Note that the information about the behavior of the function is split into \(w_1\) and \(w_2\), where \(w_1\) and \(w_2\) respectively express the effect when the first and second arguments are given. Note also that the code increment is embedded in the former predicate transformer \(w_1\).

4.2 On Recursive Programs

For recursive programs, there are clear differences between the two approaches. In the DM approach, each recursive function must be annotated with an appropriate type (which includes the predicate transformer) by a programmer, just like invariants for loops and recursive functions must be provided in deductive verification. The obtained predicate transformer is not necessarily the weakest one, depending on the precision of the annotations. In the HFL(Z) approach, no annotations are required for recursive functions, and (a predicate corresponding to) the weakest predicate transformer can be automatically expressed by using fixpoint operators.

The property above is a safety property, but one can mix the least and greatest fixpoint equations to express arbitrary regular temporal properties [9, 17], and its validity can be automatically checked (though the backend HFL(Z) validity checker is necessarily incomplete) [8].

Despite the advantages mentioned above, the HFL(Z) approach has also a disadvantage: automated HFL(Z) validity checkers used in the approach are much less efficient and less predictable than SMT solvers used in the DM approach. The inefficiency and unpredictability are inevitable because HFL(Z) validity checking is undecidable in general. In contrast, the DM approach uses the annotations to reduce the validity checking problem to simpler problems that can be discharged by ordinary SMT solvers. In fact, there are programs that the HFL(Z) approach cannot verify in realistic time, but given appropriate annotations, the DM approach can verify; see Section 5.2 for such an example. The DM approach allows modular verification; by using type annotations, the whole verification problem can be decomposed into small pieces of verification conditions.

5.1 Overview of Our Approach

In general, given (i) a main formula \(\varphi \), (ii) a set \(D_1\cup D_2\) of fixpoint equations on \(\nu \)HFL(Z) predicates, and (iii) type environments \(\varDelta _1\) for \(D_1\) (which are automatically derived from type annotations), we can reduce the validity of \(\varphi \) to the following type checking problems, thanks to the soundness of the refinement type system for \(\nu \)HFL(Z) [6, 7].

Here, \(\varDelta \vdash ^{\texttt {RT}}\varphi :\rho \) is the type judgment relation as defined in [6] (whose details are not important here) and \( \varphi _P \) is the body of \( P \). Thus, partial type annotations enable modular verification, which is expected to be more scalable and predictable than the original HFL(Z) approach. In the above decomposition of the verification problem, the weakest predicate transformers are automatically computed and used for unannotated functions, thanks to the expressive power of HFL(Z). (In contrast, the implementation of DM in F* does seem to allow some type annotations to be omitted, but in that case, very imprecise predicate transformers would be used for unannotated recursive functions.)

5.2 Experiments

We extended the existing type-based \(\nu \)HFL(Z) validity checker, ReTHFL [6] to allow partial type annotations, and conducted experiments to confirm the effectiveness of our approach.⁸ Currently, the type annotations need to be provided for \(\nu \)HFL(Z) formulas rather than for source programs. As discussed in Section 5.1, it is easy to automatically convert the Hoare-monad-style type annotations for source programs (which may be considered a restricted form of DM-style type annotations) to type annotations for \(\nu \)HFL(Z) formulas; it is left for future work to implement such a converter to make annotations easier.

In the experiment we used a Linux server equipped with Intel Xeon Gold 6242 Processor @ 2.80 GHz, with 16 cores, and 64 GB of RAM. For each (sub-)problem, we ran each tool five times and calculated the average execution time. Since the performance of the validity checker depends strongly on the performance of the underlying Constrained Horn Clause (CHC) solver, we used both Z3/Spacer [10] and HoIce [3] as underlying CHC solvers and show only the best of their results for each problem; in other words, the reported verification times indicate those in case the backend solvers Z3/Spacer [10] and HoIce [3] are called in parallel.

As the verification target of experiments, we gathered, from a benchmark for higher-order functional program verification⁹, programs for which the current ReTHFL is slow or timeouts.¹⁰ The LOCs of the target programs varies from 10 to 153. For each program, we provided a refinement type as an annotation for one of the recursive predicates (which corresponds to one of the recursive functions in the source program). See the longer version [19] for mode details about the benchmark programs and an example of type anntoations.

Dummy

The experimental results are shown in Table 2. In the table, we show the sizes of programs and annotations in terms of bytes for a fair comparison between the sizes of programs and annotations (as it is possible to write a type annotation in one long line). The first row of each program shows the result of the original version of ReTHFL. As it is a fully automated checker, no annotations were provided. The rest of the rows show the results of our method. The “Method” column shows the name of the function annotated and the annotation size. In the rest of the columns, “X / Y” means that X is the result of the sub-problem (a) that checks the correctness of the annotation and Y is the result of the sub-problem (b) that checks the validity of the whole formula.

For all runs of each sub-problem, our tool successfully checked the validity and terminated within a few seconds. This confirms the effectiveness of our approach and the behavior of the tool is much more predictable than the fully-automated verification using the original ReTHFL. We think the size of annotations is acceptable; actually, the annotation size would become smaller, if we allow a user to provide annotations for source programs rather than for HFL(Z) formulas.

The results also support the advantage of our method over the DM approach in reducing the annotation burdens. While the DM approach requires an annotation for every recursive function, our method succeded given only one annotated function for each program.