Effectful Component-Based Synthesis]
Specification-Guided Component-Based Synthesis from Effectful Libraries

Ashish Mishra

Department of Computer Science
Purdue University

Suresh Jagannathan

Department of Computer Science
Purdue University

Component-based synthesis seeks to build programs using the APIs
provided by a set of libraries.  Oftentimes, these APIs have
effects, which make it challenging to reason about the correctness
of potential synthesis candidates.  This is because changes to
global state made by effectful library procedures affect how they
may be composed together, yielding an intractably large search space
that can confound typical enumerative synthesis techniques.  If the
nature of these effects are exposed as part of their specification,
however, deductive synthesis approaches can be used to help guide
the search for components.  In this paper, we present a new
specification-guided synthesis procedure that uses Hoare-style pre-
and post-conditions to express fine-grained effects of potential
library component candidates to drive a bi-directional synthesis
search strategy.  The procedure alternates between a forward search
process that seeks to build larger terms given an existing context
but which is otherwise unaware of the actual goal, alongside a
backward search mechanism that seeks terms consistent with the
desired goal but which is otherwise unaware of the context from
which these terms must be synthesized.  To further improve
efficiency and scalability, we integrate a conflict-driven learning
procedure into the synthesis algorithm that provides a semantic
characterization of previously encountered unsuccessful search paths
that is used to prune the space of possible candidates as synthesis
proceeds.  We have implemented our ideas in a tool called  and
demonstrate its effectiveness on a number of challenging synthesis
problems defined over OCaml libraries equipped with effectful

<concept_desc>Software and its engineering Software organization and properties </concept_desc>
<concept_desc>Software and its engineering Software creation and management Software verification and validation </concept_desc>

[500]Software and its engineering Software verification and validation

§ INTRODUCTION

Many useful programming tasks can be efficiently expressed by
intelligently composing the elements found in a library of available
APIs (or components).  Program synthesis queries, in particular, can
benefit from the ability to use library function calls in synthesizing
terms.  This observation has led, in recent years, to the development
of several useful component-based synthesis
tools <cit.>. These methods typically
use examples and/or type annotations to guide the synthesis procedure
in an enumerative fashion.

However, APIs often have effects that must be taken into account when
reasoning about their composition.  Library implementations of
imperative data structures, databases, or parsers are canonical
examples where it is natural to have effectful APIs.  In these
domains, the effects performed by APIs can impose non-trivial
constraints on the choice of synthesis candidates, and the order in
which they must be sequenced.

Ordinarily, the types associated with such functions would not expose
these kinds of effects.  A typical type for an update operation on the
state maintained by a database library instance, for example, might
simply recognize that it performs a write effect by declaring its
return type to be , without providing specific details
about how the database actually changes.  Consequently,
state-of-the-art purely type-directed component-based synthesis
approaches <cit.> when applied to these kinds of libraries
could easily synthesize unsound programs because necessary protocol
constraints are not reflected in library function types.  Simply
embellishing a library with coarse read/write effect
annotations <cit.> is also unlikely to be effective for problems
like these because the lack of fine-grained effect tracking would
require the synthesis procedure to explore an intractably large space
of possible candidate compositions, since every successful call to an
effectful operation potentially alters underlying state.

However, advances in mechanized proof assistants and automated theorem
provers have made it increasingly worthwhile for library developers to
provide detailed specifications that can be used as part of a
verification task.  For example, F* <cit.> and
<cit.> are significant efforts aimed at
developing mechanically-verified effectful libraries of
general-purpose data structures and algorithms.  In this paper, we
show how library specifications of the kind produced by these efforts
can also be effectively repurposed to guide complex component-based
synthesis tasks.

Our approach introduces a new specification-guided synthesis strategy
that interprets a library's specification (expressed in terms of
Hoare-style pre- and post-conditions) as type
specifications <cit.>, using a bi-directional search strategy to
enable scalability and precision.  Specifically, we use strongest
postcondition forward-reasoning to build larger terms from existing
ones maintained by a synthesis search context, and weakest
precondition backward-reasoning from the postcondition (the synthesis
query) to enable goal-directed search.  Alone, each process has
important weaknesses - forward reasoning lacks knowledge about the
synthesis goal, while backward reasoning has an incomplete view of the
context from which terms must be synthesized.  We show how to mitigate
these weaknesses, and exploit their underlying synergies, by
integrating both within a unified synthesis framework.  For improved
efficiency and scalability, we additionally leverage a
conflict-driven learning
strategy <cit.> in the context of
effectful program synthesis, to build a knowledge base that records
discriminating propositions associated with previously
encountered incorrect synthesized terms that can be used to more
intelligently guide the search process and safely prune the space of
possible candidates we need to consider.  The need for such careful
integration arises from the unbounded search space that must be
explored to satisfy a query - having effectful libraries means that
every call to a library method in a synthesized term can potentially
result in a new heap state that reflects the effectful behavior of the
method, leading to a potential explosion of possible candidate
programs that the synthesis procedure may have to consider.

This paper makes the following contributions:

* We present a novel bi-directional deductive synthesis strategy
for specification-guided component synthesis of effectful libraries.
The synthesis strategy alternates between forward and backward
enumerative search, seeking to compose terms consistent with library

* We address scalability issues by additionally integrating a
CDCL-style learning component that builds a knowledge base of failed
candidate terms that can be used as search proceeds to avoid
reconsideration of previously identified infeasible terms.

* We present detailed experimental results on an implementation of
these ideas called  that enables component-based synthesis of
OCaml libraries equipped with effectful specifications.  Our results
demonstrate the utility of our approach over a range of different
application domains with respect to both expressivity of the
synthesis queries that can be handled, and scalability over the size
of the search space that must be navigated.

The remainder of the paper is organized as follows.  In the next
section, we provide a detailed overview of our approach.
Section <ref> presents a declarative bi-directional
type-checking formulation of the synthesis procedure.
Section <ref> formalizes the synthesis algorithm along with
details of the CDCL-learning approach used to improve enumerative
search.  Additional details about the implementation, along with
benchmark results, are presented in Section <ref>.  Related
work is given in Section <ref>, and conclusions are presented
in Section <ref>.

An overview of the  synthesis process.

Figure <ref> depicts 's synthesis procedure and its
core components. takes as input a Hoare-triple style query
specification $\Psi$ and a set of library function specifications
$\Sigma$.  For $\Sigma$, we rely on available verified effectful
libraries like  <cit.> that come equipped with effectful
specifications; from a user's perspective, a Cobalt user thus only
needs to provide a declarative specification for the synthesis goal.
More concretely, consider Figure <ref> which presents a
small library with a few functions () whose
specifications highlight how they manipulate two mutable references:
an integer res, and a boolean flag.  To ease the
presentation, each of these functions is defined to not take any
arguments.  A simple yet interesting synthesis query can be: synthesize a program, such that if it terminates when run in a
heap where  is 0 and flag is clear, updates the value of
to .

res : ref int;
flag : ref bool;

m1  : unit -> res = 0 v : int  res' = 5
m2  : unit -> res <= 20  v : int  res' = 25
m3 :  unit -> res = 5 $\wedge$ flag = false
v : int
res' = res + 2 $\wedge$ flag' = true

m4  : unit -> res = 25 v : int res' = res + 5
m5  : unit -> res = 25 v : int res' =res + 10
m6  : unit -> res = 7   v : int res' = res + 3
m7  : unit -> res > 8   v : int res' = res + 3

$\Sigma$ : Effectful specifications for a synthetic library.

This natural language query can be specified as follows in 's
specification language, where primed variables represent the input
variable values in the output heap.
goal :  res = 0 $\wedge$ flag = false (v : unit) res' = 10;

Note that because there is no function satisfying this specification
in $\Sigma$, the synthesis procedure will try to synthesize a straight
line program that uses methods from the library to satisfy the goal.

first invokes the backward-synthesis component that uses
the post-condition of the goal, and applies weakest-precondition style
reasoning to synthesize a term $e$ such that either a) $e$ satisfies
the required goal. or b) $e$ is a partial program that can be passed
to the forward-synthesis component along with a new specification
$\Psi'$. Intuitively, at each step Backward searches for a
function in the library, such that its specification allows for valid
weakest-precondition reasoning for the given post-condition. In this
example, because there is only one such function, viz. m6,
backward synthesis starts by generating a a partial term (a term with
holes) term ($\lambda$ (). (??) : unit; m6 ()). It then
continues (trying to fill the hole) to find the next such function,
creating a bigger programs in a backward fashion, consequently
generating the term ($\lambda$ ().(??) : unit ; m3();
m6()). At this point, backward-synthesis can make no further
progress as this term is neither the required goal program nor are
there any other function calls which can be synthesized via
weakest-precondition analysis. At this point we call the forward-synthesis procedure with this term and a new query spec
$\Psi'$ and an outline of the remaining program (a program with hole
$\lambda$ (). (??)  : unit), called the hypothesis $H$.

Forward synthesis has two subcomponents that collectively attempt to
synthesize a term $e'$, which when unified with $e$ gives the required
solution. If it fails to find such a term, it again invokes the Backward component with information about the failed program.
Forward synthesis uses strongest post-condition reasoning to
synthesize a term in a forward fashion.  Intuitively, it searches
for the next function which can be called in the given state, creating
bigger programs and tries to reach the required goal specification.

However this naìve search is likely to be inefficient as the search
space is likely to be intractably large, while the space of solutions
is likely to be very sparse.  To illustrate, Figure  <ref>
shows an exploration tree of the search space using a depth-first

Search space exploration without CDCL.

Search space exploration with CDCL.

This exploration does not learn from the failed (incorrect programs);
for instance, note that the exploration explores a path (shown with
shaded arrows) and synthesizes a program m7();m2(); m4() that is
incorrect (wrt $\Psi'$) but for which there are no further bigger
programs possible. In this case, the search must backtrack.  In doing
so, it finds that both programs rooted at m2, i.e. (m7();m2(); m4()) and (m7();m2(); m5()) are also
incorrect. However, durig a subsequent exploration, search again
encounters a similar subtree of incorrect programs. In fact, such
patterns would appear an arbitrary number of times, e.g., (m7();m7(); m2()...), (m7();m7(); m7();m2()...), etc.

Unfortunately, these common incorrect sequences cannot be
syntactically pruned or eliminated from subsequent searches as each
subtree occurs in a different context. Furthermore, since exploration
is costly, involving multiple calls to a theorem prover or constraint
solver, it is critical that we minimize the number of failed searches,
and avoid encountering previously examined sub-paths.  In order to
prune out such repetitive failing explorations, includes a
conflict-driven learning based component <cit.> (CDCL)
integrated with forward synthesis that allows us to searche a much
smaller space, as shown in Figure <ref>.  Using a
forward+CDCL synthesis, quickly finds that the function m1() which when sequenced with m3; m6() gives the required

Running on this synthetic example using all components
(i.e. backtrack+forward+cdcl) takes 5.08 seconds; forward-alone
synthesis (i.e. forward+cdcl) finds a solution in 7.11 seconds; a
forward-no-cdcl synthesis strategy that explores many more paths
(XX vs YY) takes 20.15 seconds, while a backward-alone
synthesis fails to find a solution.

§ OVERVIEW

An overview of the  synthesis process.

Figure <ref> depicts 's synthesis procedure and its
core components. takes as input a Hoare-triple style query
specification $\Psi$ and a set of library function specifications
$\Sigma$.  For $\Sigma$, we rely on available verified libraries like
<cit.> that come equipped with effectful specifications;
from a user's perspective, a Cobalt user thus only needs to provide a
declarative specification for the synthesis goal.

To motivate our approach, consider a string  data
structure adopted from  <cit.>
and implemented using a mutable string list in an ML-like language. The
table maintains the invariant that its elements are pairwise
distinct. It provides a set of effectful library functions to add a
new string, to check membership, etc. on a table instance. These
components have associated specifications capturing their semantics as
shown in Figure <ref>.

type pair = Pair of float * int
type table = [string] ref

add_tbl : (tbl : table * s : string) ->
$\forall$ h, Tbl. sel (h, tbl) = Tbl $\wedge$ not (mem (Tbl, s)
v : unit
$\forall$ h, v, h', Tbl, Tbl'.
sel (h', tbl) = Tbl' $\wedge$ sel (h, tbl) = Tbl $\wedge$
mem (Tbl', s) $\wedge$ size (Tbl') == size (Tbl) + 1;

mem_tbl : (tbl : table * s : string) ->
true    v : bool
Tbl' = Tbl $\wedge$ ([v=true] <=> mem(Tbl', s)) $\wedge$
([v=false] <=> not (mem (Tbl', s)));

size_tbl : (tbl : table) ->
true v : int Tbl' = Tbl $\wedge$ v == size (Tbl);

fresh_str : unit ->
true v : string mem (Tbl', v) = false $\wedge$ Tbl' = Tbl;

avg_len_tbl : (tbl : table) ->
size (Tbl) > 0 v : float  Tbl' = Tbl $\wedge$ minmax (Tbl', v);

clear_tbl : (tbl : table) -> true v : unit size (Tbl') = 0;

(* remove less than *)
rlt_tbl : (tbl : table * s : string) ->
true v : unit  size (Tbl') <= size (Tbl);

(* remove greater than *)
rgt_tbl : (tbl : table * s : string) ->
true v : unit  size (Tbl') <= size (Tbl);

Effectful specifications for a  library.

(*A Safety Query-Spec*)
$\mathtt{goal1}$ :  (tbl : table * s : string) -> v:float

(*A Functional Query-Spec*)
$\mathtt{goal2}$ : (tbl : table * s : string) ->
v : pair
$\forall$ h, v, h, h', Tbl, Tbl'.
sel (h, tbl) = Tbl $\wedge$ sel (h', tbl) = Tbl' $\wedge$
mem (Tbl', s) $\wedge$
size (Tbl') = size (Tbl) + 1;

(*A Correct Solution*)
$\mathtt{goal2}$ (tbl : table * s : string) =
b1 <- mem_tbl (tbl, s);
if (b1)
then s1 <- fresh_str ();
_ <- add_tbl(tbl, s1);
x1 <- average_len_tbl (tbl);
y1 <- size_tbl (tbl);
return Pair (x1, y1)
else _ <- add_tbl (tbl, s);
x1 <- average_len_tbl (tbl);
y1 <- size_tbl (tbl);
return Pair (x1, y1)

Functional query-spec and a solution.

Effectful specifications for a  library, Synthesis Queries and a Solution

To capture the effectful behavior of these functions, we use
specifications that express pre- and post-conditions over abstract
heaps. For instance, the specification for the add_tbl
function (refer Figure <ref> has a precondition that defines a stateful constraint on its
input string s, requiring that it not be present in the table
referenced by tbl in the input heap; specifications express
these constraints in terms of first-order predicate logic formulae
built from interpreted select/update operators <cit.> on
the heap (such as ) and user-defined uninterpreted
function symbols like  and  defined over
tables.  The postcondition captures the behavior of adding s to
the table, assuming the precondition holds, by relating the state of

A pictorial representation of the effects induced by a call to add_tbl.

the table after the function completes () to its state on
entry (); specifically, it constrains the size of
to be one more than , and asserts that
is a member of .  The  and
heap objects are accessed via input heap  and
output heap , respectively[We capitalize variables
that correspond to ghost state in specifications; these are
intermediate computed heap values that do not appear as arguments or
results of library functions.].  The specifications given for other
library functions are similar but simplified to reduce clutter. For
instance, we drop quantifiers when obvious and assume Tbl and
Tbl' represent the table tbl in pre- and post-heap h,
h', respectively.

Figure <ref> depicts the behavior of the
add_tbl (tbl, s) library function over an input example table.
The reference tbl refers to a table (a list of strings) named
Tbl before the execution of the function.   An invocation add_tbl (tbl, Dec) is executed provided the precondition that
the string to be added () is not in Tbl is true. If so, the functions adds the string to the
table, yielding the post-state in which  now refers
to a new table (labeled as Tbl').

Synthesis Problems
Given this library, there are two kinds of synthesis queries (query-specs) that can be made.  One is a type inhabitation query
similar to what is possible in other type-directed component-based
synthesis approaches <cit.>. We call these queries
safety queries since the synthesis goal is to generate a
type-safe term using library components.  Figure <ref>
shows such a query () for a function that given a table
instance and as arguments returns a .  A solution to
this query might be a function that applies  to the
goal's arguments and returns the average length of the new table via

Our focus in this paper, however, is on solving richer queries that
exploit interesting effect-based functional correctness properties
desired of the client program. For instance, our goal might be to
synthesize a function that adds its input string to a table, returning
a pair of the average length and size of the new table. These kinds of
effectful queries can be specified using a query-spec such
as the one for  shown in Figure <ref>.

This goal specifies a function that takes a table instance
() and string parameter (s) as arguments and whose
body satisfies the provided pre- and post-conditions. The
precondition imposes no constraints on the table or string.  The
postcondition is a relation between the table in the pre-heap
() and the post-heap (); it requires the
synthesized function to produce a  whose size is one
greater than  and that contains the string .
The result type of the function, however, additionally requires that
the function return a pair of  and
values.  Observe that there are no functions in the given interface
that explicitly returns a pair, although  returns the
size of the table as an , and
returns a value of type , provided that its table argument
is not empty.

§.§ Solution Overview

To explain how  synthesizes a suitable function (shown in
Figure <ref>) given these various constraints, we first
explain the details of its bi-directional search strategy and
CDCL-inspired search algorithm.

§.§.§ Weakest Precondition Guided Search

The synthesis procedure begins in a backward phase, starting
from the query's postcondition and return type.  It maintains a
context, a list of library functions and arguments provided by
the user in the query-spec, as well as path conditions.  The
procedure searches for a function f under an initial context
that contains the arguments declared in the query (e.g. s) and
libraries, such that f can be invoked in this context, leading
to the required postcondition. To make this decision,  uses a
weakest precondition call rule and performs the following check,
assuming the library specification for f is ($\overline{x_i :
\tau_i}$) $\rightarrow$ {$Pre_f$} v : t {$Post_f$}:
$\forall$ h. ([$y_i$/$x_i$]$Pre_f$) h =>
($\forall$ v:t. h'. ([$y_i$/$x_i$]$Post_f$) h v h' => Post h v h')

Given synthesized arguments $y_i$, it searches for a function $f$ to
which these arguments can be applied such that $f's$ precondition is
satisfied by the existing context, and $f$'s postcondition implies the
postcondition of the query.  To illustrate, suppose we have a query goal
($y_i$ : int) ->  dom (h, i) = true v : 'a  $y_i$ $\geq$ 5 $\wedge$ sel (h', i) $\leq$ 20

If the synthesis procedure context includes a condition (x
$\geq$ 10), then given two functions with signatures,
$f$ : (x : int) $\rightarrow$  true  v : int  x == 10 $\wedge$ sel (h', i) == 10
$g$ : (x : int) $\rightarrow$  true  v : int  x == 4

the synthesis procedure synthesizes the call, $f$(), discarding the synthesis
candidate $g$().
Note that this is a very strong requirement since the postcondition
might impose additional constraints not considered by $f$. For
instance we might have a situation where the above check does not
hold, but in which  can be translated into a form R
$\wedge$ Post' where R is a frame <cit.>. In
such a case, we can choose a function candidate if it satisfies the
following weaker check:
$\forall$ h. R $\wedge$ ([$y_i$/$x_i$]$Pre_f$) h =>
($\forall$ v:t. h'. ([$y_i$/$x_i$]$Post_f$) h v h' => Post' h v h')

This is an instance of a framing problem and in
Section <ref>, we discuss important optimizations that
allow us to soundly weaken this rule to allow partial satisfaction of
the query's goal.

If  does not find any effectful function satisfying the check,
it searches for a pure function with the required return type and
generates a subprogram with holes called hypotheses and a
weakest precondition for this pure function call.  In our example,
there is no effectful library function that immediately satisfies the
goal.  Thus,  chooses the pure Pair constructor and
generates a term represented by the following derivation:
[caption=A backward (postcondition)-guided derivation; we omit
introduction of the table instance  for perspicuity -  and
represent 's value in the pre- and post-heap, resp.,captionpos=b,label=lst:bwsearch,basicstyle=,language=ML]
[(s: string)] $\vdash$ True (v : pair)
size (Tbl') = size (Tbl) + 1 $\wedge$ mem (Tbl' s)
[(s: string)] $\vdash$
x1 <-  (??) : float; y1 <- (??) : int
size (Tbl') = size (Tbl) + 1 $\wedge$  mem (Tbl', s)
return Pair (x1, y1)

The derivation is of the form,

\[
\Gamma \vdash \{\textsf{P}\} (v : \tau) \{\textsf{Q}\}) \leadsto (\Gamma\ \vdash \{\textsf{P}\} H; \textsf{WP} (t, \textsf{Q}) \mid t'\]

and yields a hypothesis $H$, a possibly holed term,
along with a predicate (($t$, )) constructed by
applying the weakest precondition semantics for the term chosen by the
synthesis algorithm; in the above example, $t'$ = .  Since there are no available terms in the context
corresponding to the required constructor arguments (an
and ), a new term is created with two holes of
appropriate argument types; these terms are bound to fresh variables
and used as arguments to the  constructor.  Thus, $H$
captures potential program shapes for the current synthesis choice.
Observe that neither  nor ,
which can contribute to the appropriate return type, have
specifications that align with the currently synthesized term; for
example, , although returning a ,
also requires that its input table size is greater than 0, a property
that is not ensured by the holed term's precondition ().

Consequently, further progress on the backward derivation stalls.
Rather than aborting and searching for a new candidate, we instead
proceed to apply a forward search starting from the existing
precondition of the current term.  To make sure that we avail of
the information learnt from the backward derivation, we
pass $H$ (the sequence of holed terms constructing  and )
and the current weakest precondition -
size (Tbl') = size (Tbl) +1 $\wedge$  mem (Tbl', s) -
as the new postcondition for the forward search.

Although our backward search in this example simply does a pattern
matching over the data constructor Pair, our synthesis procedure
can, in fact, generate interesting non-trivial programs of larger size
by searching for a function in the library iteratively at each step,
such that its specification allows for valid weakest-precondition
reasoning for the given post-condition.  For instance, consider a
simple synthetic example with two library functions,  and

res : ref int;
flag : ref bool;
m1  : unit -> res = 7   v : int res' = res + 3

m2 :  unit -> res = 5 $\wedge$ flag = false
v : int
res' = res + 2 $\wedge$ flag' = true

These specifications highlight how the functions manipulate two mutable references:
an integer res, and a boolean flag.
Given this library and the following goal query:
goal :  res = 0 $\wedge$ flag = false (v : unit) res' = 10;

backward synthesis starts by generating a partial term (a term
with holes) ($\lambda$ (). (??) : unit; m1 ()) as the
specification for m1 satisfies the weakest-precondition check.
It then continues trying to fill the hole to find the next such
function with (WP( m1 (), {res' = 10}) as an updated
postcondition.  Now, the specification for m2 satisfies this
check and thus a bigger program is created, consequently generating
the term ($\lambda$ ().(??) : unit ; m2(); m1()), before
passing the synthesis to the forward-synthesis component.

A partial forward enumeration. gray
edges show type- and/or specification-incorrect discarded
transitions, black  edges show type-correct, potentially
explorable transitions, and red-dashed
edges give examples of type-correct paths that do not lead to required solution. Labeled nodes with same color show equivalent-modulo-stuckness nodes.

Forward synthesis has two subcomponents (refer Figure <ref>) that collectively attempt to
synthesize a term $e'$, which when unified with the partial term $e$, synthesized by the backward synthesis, gives the required
solution. If it fails to find such a term, it again invokes the Backward component with information about the failed program.
Forward synthesis uses strongest post-condition reasoning to
synthesize a term in a forward fashion.

§.§.§ Strongest Postcondition Guided Search

Because the body of the function being synthesized may contain
top-level conditional branches or match-case statements, search begins
by first synthesizing the body of the function as a top-level
branching term.  Specifically,  looks for functions with Boolean
return types, or arguments in the query-spec that have inductive type
(like lists, trees, etc.) and applies proof rules for if-then-else and match respectively to introduce top-level
conditional branching or matching synthesis sub-problems.

For instance, given the specification in Listing <ref>,
and the specification for Boolean-valued library function mem_tbl (refer Figure <ref>), generates the
synthesis sub-queries shown in Figure <ref> by applying
an if-then-else synthesis rule and introducing true and false
postconditions from 's specification to the
preconditions of the term's true and false branches
(shown in red).  We now explain how  proceeds with the synthesis
query for the true branch.  The enumeration procedure is
conceptually similar to the backward derivation, but uses the
strongest postcondition of the already-built term to guide the choice
of the next library component candidate.  Intuitively,
iteratively builds type-correct program terms of increasing
length in a depth-first manner until it finds a program that satisfies
the hypotheses (the holed terms), and the required specifications.
Not surprisingly, the domain of such terms is unbounded since we can
generate distinct unrolled looping terms like $t_1;{t_2}^{*};t_3$,
${t_1;{t_2};t_3}^{*}$, etc. of arbitrarily large depth.  To mitigate
this situation, we bound the maximum depth of search to a depth value
k on the length of program terms.  The value of k can be
chosen by the user and can be iteratively incremented.  For ease of
presentation, assume (k = 5) for our running example.
$\lambda$ (tbl : table, s : string).
b1 <- mem_tbl (tbl, s);
if (b1) then
$\forall$ h. sel (h, tbl) = Tbl $\wedge$ $\textcolor{red}{(mem (Tbl, s)}$
(x1 <- (??) : float; y1 <- (??) : int
size (Tbl') = size (Tbl +1) $\wedge$ mem (Tbl' s)
$\forall$ h. sel (h, tbl) = Tbl $\wedge$ $\textcolor{red}{not (mem (Tbl, s)}$
(x1 <- (??) : float; y1 <- (??) : int
size (Tbl') = size (Tbl +1) $\wedge$ mem (Tbl' s)

A partial program with holes and top-level branching.

Suppose during enumeration we have synthesized a term $t$ of size less
than k.  The procedure first tries to verify if $t$ is the
required solution by performing two checks that ascertain whether: a)
$t$ satisfies the hypothesis $H$ ($t$ $\prec$ $H$); and, b)
(, $t$) $\Rightarrow$
, where  and  are pre- and
post-specifications for the query specification.  Informally,
$t\ \prec\ H$ if $t$ is a term that has the same shape as $H$
with every holed term replaced by a type-consistent concrete

If $t$ satisfies these checks, the procedure returns $t$ as the
required solution. However, if either of the two checks fail, a search
commences to look for a component  that can be sequenced
with $t$. To guide this search,  uses a strongest postcondition
call rule and performs the following check, assuming the library
specification for  is ($\overline{x_i : \tau_i}$)
$\rightarrow$ {$Pre_f$} v : t {$Post_f$}:

$\forall$ h. (SP (P, t)) h => ([$y_i$/$x_i$]$Pre_f$) h

To illustrate, consider again the example scenario discussed in
the previous section. Suppose we have a query; goal:
($y_i$ : int) $\rightarrow$  dom (h, i) = true  v : 'a  $y_i$ $\geq$ 5 $\wedge$ sel (h',  i) $\leq$ 20

and that the synthesis procedure context includes the
condition, x $\geq$ 10, possibly learnt from a
conditional expression.  Given two functions with signatures:
$f$ : (x : int) $\rightarrow$  x $\leq$ 20  v : int  x == 10 $\wedge$ sel (h',  i) == 10
$g$ : (x : int) $\rightarrow$  x $\leq$ 5  v : int  x == 4

the synthesis procedure synthesizes the call $f$ (),
discarding the synthesis candidate $g$().

Figure <ref> presents a pictorial representation of this
enumeration process for some of the true branch paths of the
synthesis query.  Each choice made by the search process is given a
label (). The edges include black edges representing
explored edges as well as gray edges showing discarded choices
encountered by the forward call-rule. For instance, edge () is disallowed since the branch precondition
() is inconsistent with the precondition for
(add s). Similarly, we have other discarded edges like
(), etc.  The rule thus allows the search procedure
to discard multiple incorrect programs early on; for instance, given
the initial query above, prunes out incorrect paths such as
thereby significantly reducing
the search space of possible candidates.

§.§.§ Conflict-driven learning based enumeration

While the forward (similarly backward) search process can prune out
many incorrect programs quickly, the number of candidate programs
(paths with black edges in the figure) is likely to be still very
large, making a naïve enumerative search over this space
infeasible.  A primary reason is the likelihood of repeated
exploration of previously seen paths allowed by forward reasoning that
do not lead to the goal postcondition. For instance, consider the path
().  Here, the corresponding
program term is not a solution since the postcondition of the
synthesized term:

$\exists$ Tbl1, Tbl2, Tbl3. $\forall$ Tbl, Tbl'.
Tbl1 = Tbl $\wedge$ size (Tbl2) <= size (Tbl1) $\wedge$
size (Tbl3) <= size (Tbl2) $\wedge$
size (Tbl') = 0

does not imply the postcondition of the true branch of the current
synthesis candidate, which requires that

size (Tbl') = size (Tbl +1) $\wedge$ mem (Tbl'
Further, since the depth of the path when reaching
(here, 4) is less than the depth-bound (k=5), the search process seeks
a component that can satisfy the required postcondition.
Unfortunately, no such choice is possible. Thus, the algorithm
backtracks and makes a different choice at one of the earlier
nodes. We call a node like  that can no longer make
progress for a given k as a k-bound-stuck-node, inspired
by the notion of a conflict-node in conflict-driven learning
approaches <cit.>.

Suppose, the algorithm backtracks to node  (over multiple
steps); unfortunately, it again faces a choice similar to the choice
at the stuck-node  to select/discard the function clear_tbl.  Since the term corresponding to path () (call it $t_1$) is syntactically distinct from the term
corresponding to () (call it
$t_2$), the algorithm cannot trivially prune out this choice.  But, by
choosing , it must again performs checks similar to those
performed under the $k$-bound-stuck-node . For instance,
the algorithm would again visit discarded terms (gray edges) like
(add_tbl(tbl, s), avg_len_tbl (tbl), etc.). Finally, it will
eventually find itself at another $k$-bound-stuck node
() causing it to backtrack to .  Once again,
it faces a choice (), which is similar to the new
stuck node found at ().  Figure <ref>
depicts how the algorithm repeatedly traverses many paths similar to
an already visited stuck path, and must therefore eventually

Even though concluding the similarity between $t_1$ and $t_2$ is not
possible syntactically, we observe that this similarity arises because
the algorithm is making the same function choice (i.e. ) and the strongest postconditions  and
that guide the search process under
and  are related by .  In an unbounded depth-first search (k=$\infty$), for
any path explored under , there exists a path explored
under , and hence by knowing that  does not lead
to a solution (i.e. is a $k$-bound-stuck-node), we can conclude that
will also not lead to a solution.  We can, therefore,
discard the exploration of the tree rooted at  by learning
the postconditions at  and . We call nodes like
( and ) as equivalent-modulo-stuckness,
and highlight their similarity by depicting them with the same color
in Figure <ref>.

However, since our exploration is bounded by terms of size k,
there may be paths that were prematurely truncated under
but can make progress under . For example, consider a path
() under .  Eagerly discarding
would lead us to miss such paths and may result in failure
to satisfy a feasible synthesis query under a given k bound.
Notice, however, that for each such path under , there is a
smaller path e.g. () that is also reachable and
can lead to a solution if the longer path under  can.  Thus
and  can be assumed to be logically
equivalent-modulo-stuckness; we can thus safely discard the
exploration of the tree rooted at , given that there is an
equivalent path at .

Based on the above observations, we equip our search procedure with a
conflict-driven learning component called CDCL-search that
learns discriminating propositions ($D^{k}$ ())
associated with each visited k-bound-stuck-node Fi and
uses them to discard future exploration of nodes that are logically
equivalent to an earlier k-bound-stuck-node, modulo the stuckness

We explain the working of the algorithm using our running example.
Upon encountering a k-bound-stuck-node (e.g. node F7), our CDCL
search procedure learns two propositions.  First, it learns a
proposition $S_p$, which we call the stuck-path proposition that
captures the post-state for the k-bound-stuck-node (e.g. F7).
Second, it creates a disjunctive formula $T_p$ called truncated
proposition containing a disjunct for each call truncated
prematurely for the k-bound-stuck-node (e.g. F7 -> fresh_str).
The idea is to learn information about paths that were taken but were
prematurely left unexplored due to the bound $k$.  The
discriminating proposition for a k-bound-stuck node $D^{k}$
(k-bound-stuck-node) is given by a tuple ($S_p$, $T_p$).

$\Bigg\{$not ( $\forall$ Tbl'. size (Tbl') = 0  =>  size (Tbl') = 0) $\Bigg\}$ $\vee$
$\Bigg\{$($\forall$ Tbl, Tbl'. ... $\wedge$ size (Tbl') = 0  => true $\wedge$
(not ($\forall$ Tbl, Tbl'. size (Tbl') <= size (Tbl) => true)) $\Bigg\}$

Checks derived using the discriminating proposition $D^{k}$ () in CDCL-search.

$D^{k}$ () can help us to discard logically equivalent-modulo
stuck nodes: the algorithm backtracks with this learned information to
the earlier decision node ; while making the decision at
edge () with the $D^{k}$ () information in hand,
the algorithm checks if the decision node  is logically
equivalent-modulo-stuckness with the earlier encounter of clear_tbl(tbl).
The algorithm performs the following checks, where $t_3$ is the term
corresponding to path (), and $\den{\textsf{F7}}$ =
, the function invoked at node  in Figure <ref>:

(not ( $D^{k}$($\den{\textsf{F7}}$).$S_p$ => SP (P, $t_1$)))  $\vee$

(SP (P, $t_1$) => $D^{k}$($\den{\textsf{F7}}$).$T_p$ $\wedge$

not (SP (P, $t_3$) => $D^{k}$($\den{\textsf{F7}}$).$T_p$))

Intuitively, these two disjuncts check the two observations discussed
earlier.  The first disjunct captures the fact that any path that can
be explored by making this choice was already visited and seen to be
leading to a stuck-node under the earlier exploration of clear_tbl(tbl)
at .  The second disjunct verifies that for any node that
was truncated prematurely under the stuck-node and that can make
progress under the current choice, there is an equivalent path in a
tree rooted outside .  For our running example, this
translates and simplifies to checks shown in Figure <ref>.
Since both these disjuncts are false, the CDCL-search algorithm
decides that for the current value of k, the two nodes are
logically equivalent-modulo-stuckness and  it can thus safely discard
the exploration of .

The forward-algorithm continues the exploration with learning until it
finds a solution for the given value $k$.  If it fails to find a
program, it returns the failed paths of lengths upto k to the
backward search again, in a handshaking step.  At this point,
the backward algorithm may need to backtrack and make different
choices.  By supplying failing information about paths, the backward
search can avoid choosing equivalent terms modulo these failures.  We
depict the various components of the synthesis procedure in
Figure <ref>.  Applying these mechanisms (backward+forward+cdcl) to the original
goal (),  synthesizes the solution shown in
Figure <ref> in approximately 7 seconds.

(i.e. forward+cdcl) finds a solution in 10 seconds; a forward-no-cdcl
synthesis strategy explores many more paths (compared to forward+cdcl)
and takes 28 seconds, while a backward-alone synthesis strategy fails
to find a solution within a 10 minute time-bound.

§  SYNTHESIS

ottfundefnblock[3][]    #3

We now present a set of bi-directional search rules and the
CDCL-search algorithm presented in the last section that formalizes our
specification-guided synthesis strategy.

Synthesis Language.
Our synthesis procedure operates over a core-calculus
$\lambda_{\eff}$ <cit.>, an extension of
the call-by-value simply-typed $\lambda$-calculus tailored to support
specification-guided component-based synthesis.  The language
differentiates between pure and impure expressions, the latter being
those whose computation can induce effects.  Values are constants of
base type, type constructor applications, (closed) lambda expressions,
and locations.  Pure expressions are values and variables.  Impure
expressions include calls to effectful library functions, expressions
that create references, pattern-matching and conditional expressions
whose bodies may introduce effects, a monadic return expression, and
and a monadic sequencing expression (x $\leftarrow$ $_1$ ;
$_2$) that evaluates $\eip_1$ and binds its result to a variable
x in $\eip_2$.

c $\in$ Constants

$\in$ Variables

$\ell$ $\in$ Locations

v $\in$ Value     ::=     c $\mid$ $\ell$ $\mid$ $\lambda$ (:$\tau$). $\mid$ $\mathsf{D_i}$ $\overline{x_{j}}$

$\ep$ $\in$ Pure Exp     ::=      $\mid$

$\eip$ $\in$ Impure Exp     ::=       ($\overline{\ep}$) $\mid$  $\mid$  match with $\mathsf{D_i}$ $\overline{\mathsf{x}_{j}}$ $\rightarrow$

$\mid$ if  then  else $\mid$ return $\mid$  $\leftarrow$ $_1$; $_2$ $\mid$ $\diamondsuit$

$\in$ Library Function

$\diamondsuit$ $\in$ hole	    ::=      (??) : $\tau$

TN $\in$ TypeNames     ::=      list, tree, pair,

t $\in$ Base-Type     ::=     int $\mid$ bool $\mid$ …$\mid$ heap $\mid$ TN  $\mid$

$\tau$ $\in$ Type     ::=     {$\nu$ : t | $\phi$ } $\mid$ ( : $\tau$) $\rightarrow$ $\tau$  $\mid$ { $\phi_1$ } $\nu$ : t { $\phi_2$ }

$\phi$,$P$,$Q$ $\in$ Propositions     ::=      $\mid$  $\mid$

$\mid$ $\neg$ $\phi$ $\mid$ $\phi$ $\wedge$ $\phi$  $\mid$ $\phi \lor \phi$  $\mid$ $\phi$ $\Rightarrow$ $\phi$ $\mid$ $\forall$ (x : t). $\phi$ $\mid$ $\exists$ (x : t). $\phi$

$\Gamma$ $\in$ Type Context     ::=     $\varnothing$ $\mid$ $\Gamma$, x : $\tau$ $\mid$ $\Gamma$, $\phi$

$\Sigma$ $\in$ Library     ::=     $\varnothing$ $\mid$ $\Sigma$, $f$ :
($\overline{x_i : \tau_{i}}$) $\rightarrow$ $\tau$

$\mid$ $\Sigma$, $\mathsf{D_i}$ $\overline{x_j :
\tau_{j}}$ $\rightarrow$ $\tau$

$\lambda_{eff}$ Expressions and Types

As we have seen in our earlier examples, the language also allows
typed holed-expressions of a given type $\tau$ that takes the form
((??) : $\tau$).  Such a term represent an unknown expression in a
program that must be constrained by the type $\tau$; our synthesis
procedure transforms such expressions by replacing these holes with
concrete terms.

Types and Environments.

The type language includes support for base types such as types
for integers, Booleans, strings, etc., as well as a special heap
type to denote the type of abstract heap variables like h, h'
found in specifications.  There are additionally user-defined data
types , and type constructors used to type references that
hold values of some base type.  More interestingly, base types can be
refined with propositions, and effectful computations have
types defined in terms of Hoare-style pre and postconditions of the
form {$\phi_1$} $\nu$ : t {$\phi_1'$} that represents an
effectful computation, which when executed in a pre-state satisfying
proposition {$\phi_1$}, upon termination, returns a value $\nu$ of
base type t along with a post-state satisfying {$\phi_1'$}.

Propositions ($\phi$) are first-order predicate logic formulae over
base-typed variables.  Propositions also include a set of Qualifiers which are user-defined uninterpreted functions symbols
such as mem, size etc. used in our example; qualifiers also
include two special interpreted function symbols ( and
) used to model access and modification to the global
heap[Details about the language's type system can be found in
the supplemental material.]  The type language also includes
dependent-function types since arguments and return values of library
functions can be associated with types that are refined by

Propositions in pre- and post-conditions capture non-spatial
properties of the pre- and post-abstract heaps respectively.  These
properties capture actions involving accesses and modifications to
heap objects associated with a heap variable (sel and update), or describe shallow structural properties of heap objects,
e.g., length, head, etc. for a list.  Our current implementation
currently does not allow expression of spatial properties that
describe disjointedness of heap fragments.  Consequently, we assume that
each heap object is always referenced by a unique path (variable x or x.f.y) and that there is no sharing of heap objects.  We
have found that these assumptions are not particularly onerous in the
context of the OCaml libraries we have examined.

There are two environments maintained by , of particular interest
to our synthesis procedure: (1) environment $\Gamma$ records the types
of variables along with a set of propositions relevant to a specific
context, and (2) and, environment $\Sigma$ maps library functions and
datatype constructors to their signatures.

§.§ A  Synthesis Problem

A  synthesis problem can be described as follows: Given a
library $\Sigma$ of functions and data constructors, annotated with a
suitable types, a type environment $\Gamma$, and a goal specification
($\Psi$), which is a dependent-function type of the form

\[ (\mathsf{x} : \tau) \rightarrow (\{P\} \mathsf{v} : \mathsf{t} \{Q\}) \]

where v is a free variable denoting the return value of the program and pre and post-conditions $P, Q$ may contain argument variable x, heap locations and the return variable v,
the synthesis problem seeks to synthesize an expression $e \in e_p \cup e_{ip}$ in $\lambda_{\mathit{eff}}$
such that

\[\Gamma; \Sigma \vdash e :(\mathsf{x} : \tau) \rightarrow \{P\} \mathsf{v} : \mathsf{t} \{Q\} \]

§.§ Bi-directional Deductive Component-Based Synthesis

Given a  synthesis problem, the synthesis procedure is a bi-directional deductive proof-search <cit.> over
library functions and the given query specification. We next explain
each of these modes of the synthesis procedure.

§.§.§ Forward Synthesis

Forward Type Synthesis Rules

Backward Type Synthesis Rules

Forward and Backward Type Synthesis Rules

Figure <ref> shows our forward synthesis system using  synthesis rules of the following form:

\[
\Gamma  \ottsym{;}  \Sigma  \vdash  \tau  \twoheadrightarrow  \ottnt{e}
\]

Each such rule defines a declarative judgment explaining the
generation (along with a proof-derivation) of a conclusion term e in an environment of types ($\Gamma$) and libraries ($\Sigma$)
against a given type $\tau$, using the derivation of other well-typed subterms in the rule's premise. Generating a variable
(FW_Var) simply requires choosing the variable of
the required type from the environment.  To generate a match
expression (FW_Match) the procedure first
recursively generates a term e using the
(FW_Var) rule for a datatype  from the
environment. Second, it creates an extended environment $\Gamma_i$ for
each case branch i using constructors ($\mathsf{D_i}$
($\overline{\mathsf{x}_j : \tau_j}$) $\rightarrow$ { $\nu$ : TN |
$\phi_i$ } for the , while replacing the bound variable
$\nu$ in each $\phi_i$ with an existential match variable
$x'$. Finally, it recursively generates expressions ($\mathsf{e}_i$)
for the original synthesis problem specification in each of these
extended environments. Thus, the rule allows us to break the original
synthesis problem into $i$ subproblems that can be solved in
stronger environments, thereby pushing type information from a
constructor's specification (${\mathsf{D_i}}$ $\in$ $\Sigma$) to the
synthesis query.

The generation of a conditional if-then-else expression
(FW_IF) is similar to  with a few
important differences. It first requires the generation of the Boolean
test expression e. Since our focus is component-based synthesis,
the synthesis procedure only has access to the library specifications
($\Sigma$) and the goal specification $\Psi$ at its disposal. Thus,
only way to generate a Boolean-typed expression is via function
calls. Consequently, the procedure searches for a library function
call with Boolean return type using the FW_Call
rule described below and postconditions ($\phi_t$ and $\phi_f$) for
true and false return values, resp.

It then creates extended environments to recursively synthesize the
true and false branch by substituting true and false for
the bounded variable $\nu$, and synthesizes terms for the true and
false branches in their extended environments.

The FW_Call rule defines the strongest-post
condition forward search procedure.  The rule depicts a scenario when
a single function-call does not suffice to generate a term for the
required goal specification $\Psi$. It breaks the original synthesis
into two sub-synthesis problems: First, it searches for a
function $f$ in the library with a type, such that a) the synthesis
procedure can synthesize expressions $\overline{y_i}$ as its arguments (see
second premise); b) with appropriate mapping for the heap and
arguments variables[We drop variable substitutions in
propositions to reduce clutter in rules], it can satisfy the forward
rule for Hoare-style reasoning, i.e. the goal's precondition P
implies the required precondition $\mathsf{P_1}$ for $f$ (see third
premise).  Successfully checking these two conditions implies that a
function call expression ($f$ ($\overline{y_i}$)) in the current
environment is well-typed.  Second, it calculates the strongest-post
condition (SP (P, ($f$ ($\overline{y_i}$)))) for this term, and
recursively synthesizes an expression e with this as the new
precondition.  The expression synthesized for the original
specification is a monadic sequencing of the function call ($f$
($\overline{y_i}$)) and e.

The rule (FW_Frame) is concerned with expression
synthesis taking into account frames, heap/store fragments that
do not change during the evaluation of a program
expression <cit.>.

The auxiliary function Vars(R) gives the set of
reference used in $R$. The auxiliary function EVars takes a
list of propositions and returns the set of existential references
found in the environment used in these propositions; these
existentials are introduced when computing the strongest
postcondition in the FW_Call rule. The function
Qual(R) gives the set of qualifiers (like
, , etc.) used in $R$.  The premise in
FW_Frame checks that the references found in the
frame $R$ are disjoint from the existential references in $P$ and
$Q$ and that $R$'s qualifier set is also disjoint from $P$ and

The subtype rule (FW_Sub) defines the condition
for the successful termination of the forward proof search process
using the standard strongest postcondition-based verification
condition check.

§.§.§ Backward Synthesis

Figure <ref> presents the backward synthesis inference
rules whose judgments are either of the form:

\[
\Gamma  \ottsym{;}  \Sigma  \vdash  \tau  \twoheadleftarrow  \ottnt{e}
\]

for introducing a holed subterm into, or

\[
\Gamma  \ottsym{;}  \Sigma  \vdash  \{\phi_1\}\, \diamondsuit\, \{\phi_2\}  \twoheadleftarrow  \ottnt{e}
\]

for eliminating a holed subterm from, the term being synthesized.

Backward synthesis can invoke forward-synthesis non-deterministically
at any time (see rule BW_FW). In practice, we invoke
the forward rule when the backward synthesis cannot make any progress,
i.e. when no backward rule applies.

The backward hole rule (BW_hole) generates a holed
expression bound to a fresh variable $y$ for an arbitrary synthesis
query. This is the introduction rule for a holed expression that
allows the procedure to create hypotheses when backward synthesis
cannot find a required term in the context.

The main rule for backward enumeration is
BW_Call. The rule requires searching for a function
$f$ in the library with a return type matching the hole. Note the
difference from the FW_Call rule, where we looked
for any allowed function call; here, we use goal directed search
instead.  Once such a function is found, the rule generates arguments
$y_i$ for $f$ by either introducing holed terms for each argument,
effectively yielding new synthesis sub-queries, or finding suitable
variables (using BW_Var, similar to
FW_Var, not shown here) in the environment) of the
required type. This is an instance where the effect of having an incomplete view
of the context becomes apparent during the backward search.  The rule
ensures that the function call can be soundly made using the weakest
precondition check.  This check verifies that, assuming the
precondition for the function ($P_1$) in the given environment
($\Gamma$) holds, that the postcondition for the function ($Q_1$)
implies the goal postcondition ($Q$) with appropriate substitution for
heap variables and arguments[We elide variable substitutions
in the rules for perspicuity.]  If this check succeeds,
it further checks that the resulting term is not already seen as a failed program using the
set of learned failed programs F.  If successful,
the weakest
precondition predicate (WP(($f$ ($\overline{y_i}$)), $Q$)) for the
function call using $Q$ and the function's argument and specifications
is used.  Finally, it creates new subproblems using this weakest
precondition as the postcondition and the types of the function's
arguments as the hole types.

The backward frame rule (BW_Frame) identifies a frame $R$ using the
consequence judgments in the premise, applies frame rule checks on the
disjointness of variables and qualifiers, and establishes a synthesis
query on the framed pre- and postconditions ($P_1$ and $Q_1$).

§ SYNTHESIS ALGORITHM

$\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\mathtt{F}$

$t$ := BW_Rules ($\Gamma$, $\Sigma$ ,$\Psi$,

$(t \neq\ (\bot, \_) )$
return $t$

$(t = (\bot, \langle\, H, e_b, \Psi' \rangle))$
$t'$ := CDCL ($\langle\Gamma$, $\Sigma$, $\Psi'\rangle$, $H$)

$(t' = e_f)$
return ($e_f$; $e_b$)

$t'$ = $(\bot$, $\mathtt{F'})$
($\Gamma$, $\Sigma$, $\Psi$, ($\mathtt{F}$
$\cup$ $\mathtt{F'}$))

\[\]

\[\]

$\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $H$

D := $\forall$ $c_i$ $\in$ $\Sigma$. D ($c_i$) = ($\mathsf{true}, \mathsf{false}$)

$\mathtt{F}$ := $\varnothing$, $p_i$ := $\bot$

($\Gamma$, $D$, $c_i$) := $\mathcal{R}$_Choice ($\Gamma$, $\Sigma$, D,
$H$, $p_i$)

$c_i$ = $\bot$
$(\mid$ $p_i$ $\mid\ > 0)$
$\mathtt{F}$ := $\mathtt{F}$ $\cup$ {($p_i$)}
($p_i$, $D$) := $\mathcal{R}$_Learn ($\Gamma$, $\Sigma$, $\langle$ D, $p_i$

return ($\bot$, $\mathtt{F}$)

$e$ := FW_SUB ($\Gamma$, $\Sigma$,
($p_i$;$c_i$), $\Psi$)
($e$ $\neq$ $\bot$)
return $e$

$p_i$ := ($p_i$;$c_i$)

The Synthesis Algorithm

Algorithm <ref> outlines the top-level synthesis
algorithm and can be understood as pseudo-code for the overview of our
approach given in Figure <ref>. The input to the
algorithm is a  synthesis problem (a triple
$\langle\Gamma,\Sigma,\Psi\rangle$) along with a set of explored stuck-paths $\mathtt{F}$, initially empty.  The algorithm first
makes a call to the backward synthesis procedure using a function
, a deterministic implementation of the backward
synthesis rules given in Figure  <ref>). In case backward
synthesis does not succeed in producing a complete solution (line 4),
it returns a partial solution $e_b$, a hypothesis $H$, and a new
specification $\Psi'$, which is calculated by substituting the weakest
precondition for $\Psi$'s postcondition and the partial solution
$e_b$. The algorithm invokes the  routine (line 5) with
the hypothesis $H$, the updated specification $\Psi'$.  The CDCL
routine if successful, returns a solution $e_f$ for $\Psi'$, which is
then sequenced (using a monadic-sequencing expression) with the
partial backward solution $e_b$, to give the required solution for the
original problem (line 8).  Otherwise, the synthesis routine is
recursively called (line 9) with an updated stuck-paths set
($\mathtt{F \cup F'}$).

§.§ Conflict Driven Learning Based Enumeration

The CDCL routine takes as input a synthesis problem as well as a
hypothesis $H$ and returns either a $\lambda_{\mathit{eff}}$
expression satisfying $\Psi$ (line 20) or $\bot$ (line 18) if it
cannot find such an expression. It maintains three data-structures: 1)
a Discriminating Propositions map D that maps components
$c_i$ to a pair of stuck-path and truncated-path propositions as
discussed in the last section; 2) a sequence of
components $p_i$ (a path) representing the partially synthesized
expression; 3) a set of already explored stuck-paths
$\mathtt{F}$.  The algorithm begins by initializing D by mapping each
component in $\Sigma$ with trivial propositions and the sequence $p_i$
as an empty sequence.  The search is performed by the main loop (lines
12-21) that iterates until it finds a correct expression (line 20) or
has exhausted path exploration (line 18), updating D and $p_i$ in each

The algorithm makes a choice of the next component for a given $p_i$
and D, using a function $\mathcal{R}$_Choice (line 13), a
deterministic implementation of the CDCL_CHOICE rule
given in Figure <ref>.  If the procedure is unable to find a
new component (line 14), it learns new discriminating propositions for
the stuck-node associated with $p_i$ and backtracks to the previous
path using a function $\mathcal{R}$_Learn (line 17), a deterministic
implementation of the CDCL_LEARN rule in
Figure <ref>, or it has exhausted all paths and terminates
the loop (line 18).  If a candidate component has been found, a call
to the FW_Sub function (corresponding to the rule
FW_SUB in Figure  <ref>) is performed (line 19);
this call checks if the type for the expression corresponding to path
($p_i$;$c_i$) is a subtype of the original synthesis query $\Psi$, in
which case it returns this expression.  If not, the algorithm
continues with an updated path ($p_i$;$c_i$).

Learning Discriminating Propositions

We introduce discriminating propositions for a k-bound-stuck-node

$c_i$ using the CDCL_LEARN
rule. A Detailed formal definitions for k-bound-stuck nodes can be found in the technical resort <cit.>. Given a stuck-path $p_i$, typing ($\Gamma$) and library
($\Sigma$) environments, and an incoming discriminating propositions
Map $D$, the rule generates a new set of discriminating propositions
for the stuck-node $c_i$, updating $D$ in the process, and returning a
smaller path to be explored next.  The learned proposition has two
components.  The first is a stuck-path proposition $\phi_s$ that
captures the strongest postcondition for $t_{p_i}$, the expression
corresponding to $p_i$ for the given goal precondition
$\phi$.[In the following, we abuse the use of $p_i$ to serve
as both the path and the term $t_{p_i}$ it represents for
perspicuity.]  The second component, a truncated proposition
$\phi_t$, is a disjunction over the preconditions of those components
$c_j$ that can in principle be invoked using the
rule but which cannot due to the bound $k$
and which are thus prematurely truncated. This is ensured by the
implication ($\Sigma$, $\Gamma$ $\phi_s$ $\Rightarrow$ $\phi_{c_j}$).

$\begin{array}{c} H; D ; \Gamma; \Sigma  \vdash
(\Psi, p_i) \hookrightarrow (p_i;c_i) \\
\Gamma; \Sigma  \vdash (p_i, D) \hookrightarrow (p_i', D')
\end{array}$

CDCL Rules

Ψ≡{ ϕ} v : t { ϕ' }   p_i ≡c_1;c_2;...;c_i      D(f_i) = ⟨ϕ_s_f_i, ϕ_t_f_i ⟩     ϕ_s ≡𝐒𝐏 (ϕ, 𝐩_𝐢)

ϕ_t ≡{ ⋁_j. ϕ_c_j |(c_j : (x_i : τ_i) →{ϕ_c_j} v : t' {ϕ_c_j'})  ∈Σ∧(Γ, ϕ_s => ϕ_c_j)}

D' = D [c_i ↦⟨(ϕ_s_f_i ∧ϕ_s), (ϕ_t_f_i ∨ϕ_t) ⟩]
Γ; Σ;  ⊢(p_i, D) ↪((c_1;c_2;...c_i-1), D')[CDCL_LEARN]

Ψ≡{ ϕ} v : t { ϕ' }     Γ; Σ⊢{𝖲𝖯(ϕ, p_i)} 𝗏 : 𝗍 { ϕ' } ↠c_i

(p_i; c_i) ≺H   D(c_i) = ⟨ϕ_s, ϕ_t ⟩  |(p_i; c_i) |≤k      X ≡{ (ϕ_s => 𝐒𝐏 (ϕ, (𝐩_𝐢;𝐜_𝐢))} ∨

{(𝐒𝐏 (ϕ, (𝐩_𝐢;𝐜_𝐢)) => ϕ_t) ∧(𝐒𝐏 (ϕ, (𝐩_𝐢)) =>

([Γ] X)
H; D ; Γ; Σ;  ⊢(Ψ, p_i) ↪(p_i;c_i)

Rules for constructing and using discriminating propositions.

The CDCL_CHOICE rule uses the discriminating
propositions introduced by the learning rule to prune away
equivalent-modulo-stuckness paths. It returns a new function
component $c_i$

that can be used to construct a bigger
$\lambda_{\mathit{eff}}$ expression, provided an existing path $p_i$,
a hypothesis $H$, typing and library environments, a discriminating
propositions map $D$, and the goal specification $\Psi$. The rule
first searches for a component $c_i$ using the forward synthesis
rules, and performs two additional checks for the new potential path
$p_{i+1}$ = ($p_i$;$c_i$): (1) that $p_{i+1}$ satisfies the shape
given by the hypothesis $H$, and (2)
that $p_{i+1}$ is not equivalent-modulo-stuckness to some earlier
visited stuck-path. The check first generates the strongest
postconditions for the expressions corresponding to paths $p_i$ and
$p_{i+1}$ respectively.  It extracts the discriminating proposition
pair ($\phi_{s}$, $\phi_t$) for the component $c_i$ and generates a
check with two disjuncts. Failure of the first disjunct intuitively
implies that any path (and hence the corresponding term) that can be
explored by choosing $c_i$ was explored earlier without leading to a
solution and hence the exploration of $c_i$ and all the following
paths can be safely skipped without effecting the completeness of the
search process. In such a case, we should choose $c_i$ only if we had
prematurely truncated some path earlier that can also be taken along
$p_{i+1}$ (checked using conjunct #1 in the second disjunct) and
which cannot be explored without exploring $p_{i+1}$ (checked using
conjunct #2 in the second disjunct).

§.§ Soundness

Programs synthesized by  are correct with respect to the provided
query specification $\Psi$ assuming the validity of each library
function against their specifications.
Complete proofs for the theorems can be found in the technical report <cit.>.

Iff Synthesize ($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\varnothing$) = e then
$\Gamma$;$\Sigma$ $\vdash$ e : $\Psi$.

Since the CDCL routine (refer Algorithm <ref>) can possibly discard a correct program if
it can ensure that there exists another program satisfying the given query-spec of
smaller size, the completeness argument is relative to a query spec.

$\forall$ k. If Synthesize ($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\varnothing$) =  $\bot$
then $\nexists$ e. $\mid$ e $\mid$ $\leq$ k and $\Gamma$; $\Sigma$ $\vdash$ e : $\Psi$.

is implemented in OCaml with total of 7329 lines of code.
This includes $\lambda_{\mathit{eff}}$ definitions (1577 lines) and
Algorithm <ref> along with deterministic implementations for backward and forward synthesis
rules and CDCL learning and choice (3061 lines).
We rely on OCaml lexing and parsing libraries
OCamllex <cit.> for designing the front end of our query
specification language and use Z3 <cit.> for discharging the SMT
The input to  is a specification file containing a library of function and data-constructors followed by
a goal query specification.

§.§ Limitations

Think of bullet points we wish to add here.

§ IMPLEMENTATION AND EVALUATION

is implemented in approximately 7300 lines of OCaml.
We rely on OCaml lexing and parsing libraries OCamllex <cit.> for
handling the front end of our query specification language and use
Z3 <cit.> to discharge SMT queries.  The input to  is a
specification file containing a library of functions and data
constructors, along with their specifications, followed by a goal
query specification.

We evaluate by synthesizing programs from several domains and
consider its effectiveness with respect to the following questions:

$\textnormal{RQ}_1$ Is  effective in synthesizing
programs from available verified libraries?

$\textnormal{RQ}_2$ How does 's integration of forward,
backward, and CDCL search compare against each technique applied

$\textnormal{RQ}_3$ How sensitive is  synthesis to the
complexity of library specifications and queries?

$\textnormal{RQ}_4$ How does  compare against other
state-of-the art component-based synthesis techniques when
applied to specification-rich libraries?

§.§ Benchmarks

We consider a number of synthesis problems
for applications drawn from three different domains.
A detailed characterization of the queries used is provided in the
technical report <cit.>.

The results of applying  to these problem domains are shown in
Figures <ref>,  <ref> and
<ref>.  In these figures, synthesis problems
for database applications are prefixed with “D” and are
adopted from <cit.>.  These queries (D1-D11) are
defined over two database applications.  The first is a Newsletter database with a single table NS with attributes
newsletter, user, subscribed, articles, code, etc.  and
effectful library functions such as subscribe, unsubscribe,
add, etc.  An example query (D5) encodes the following problem:
given a newsletter n and a user u, return the list of articles
available to u in n, and then unsubscribe u from n; the solution
must take care to first check that the user is subscribed to the
newsletter before unsubscribing.  The second is a network firewall
database that has two tables, a table of devices and a table storing
sender-receiver links; its library functions include add_device, add_connection, delete_device etc.  For example,
query D7 encodes the following problem: insert new devices d
and x in the device table and create a connection between them.
Synthesizing programs from queries of this kind must take into
account appropriate preconditions that reflect the effectful
behavior of the library; e.g., to establish a connection to a device
that is not currently in the device table requires that the device
first be added.

The second domain consists of parser benchmarks prefixed
with “P” and include stateful combinator style parsers for
simplified grammars for a PNG image format and C-language declaration
syntax.  The libraries and specifications are constructed using the
grammars of stateful parsers  <cit.>.  The libraries include
subparsers and standard basic parsers for alphabet, identifier,
number, etc.  The synthesis queries describe the specification for
bigger parsers that can be constructed using these libraries.
E.g. benchmark P1 encodes the following data-dependent property: synthesize a parser for a png-chunk using subparsers for length,
typespec, content, etc. such that the combined size of typespec and
content of the output chunk is always equal to the parsed length
value.  Synthesizing programs that satisfy these kinds of
properties must take into account the effects of upstream parsers on
the length value when considering parsing candidates downstream in a
parsing pipeline.

The third domain considers imperative data structure libraries
that implement tables, queues written in OCaml; in the figures, these
benchmarks are prefixed with “I”.  The  library
described in Figure <ref> and its specifications are adopted
from  <cit.>, while libraries for Queue are
adopted from the development of mutable data structures given in
Software Foundations <cit.>. The queries we consider involve
multiple insertions, deletions, conditional insertions/deletions
etc. on tables and queues, maintaining library usage protocols.  For
instance, I4 encodes the following query : Given a queue of
unique integers, and an integer, synthesize a program which
increments the size of the queue.  The result must take into
account if the given integer is present in the queue or not and then
appropriately insert either the given or a new integer.

This domain also includes other OCaml data structure libraries
imported from works attempting mechanical verification for OCaml
libraries <cit.>. These benchmarks are prefixed with the
appropriate data-structure name, for instance “V” for OCaml Vector
library, “HT” for Hash Tables, etc. The queries again include
standard textbook examples of the usages of these libraries.
E.g. benchmark HT3 encodes the following query: given a hash
table, and a key-value pair, add the pair in the table, create a new
hash table and transfer the contents of the current table to the new

In total, these libraries span 48 files and contain a total of 251
functions, a size that makes memorization of their signatures and
specifications by clients impractical.

The imperative data-structure Libraries contribute 105 functions,
the parser library contributes 32, the database library contributes
40, with the remaining functions include constructors
(e.g.  and , etc.) and pure functions
from OCaml libraries like the OCaml Core <cit.> (or functions
translated from the Haskell Core libraries used by other purely
functional component-based synthesis approach <cit.>).

Note that works on this complete library set; the alternative
could be to find the minimal set of functions required for each
domain. Finding such a library set apriori is not feasible as these
functions can be called across multiple domains. E.g. a database
domain benchmark may use a List library from the imperative
data-strcture domain; a Queue benchmark may use a pure pair creation
function, etc.  Indeed, we found that 28% of our synthesized
solutions used at least one function from outside its domain.

§.§ Library Specification Annotations

All the benchmarks in our evaluation were taken from verified
libraries whose specifications were provided by the library authors.
Fortunately there are multiple such projects currently available
across a number of different
domains <cit.>.  We adopted
these specifications to the specification language, a
straightforward mechanical task for most of these benchmarks; four of
the libraries defined specifications that capture richer properties
than what  currenty supports and their specifications had to be
slightly rewritten.  For example, the specification for the
library in the  suite leverages the
algebraic theory of lists which cannot be handled using our SMT driven
synthesis.  Here, we adopted these specification to use more abstract
notions like list membership, ordering, etc. These libraries are used
in benchmarks V1-V3, Q1-Q3, RB1, RB2, and ZL1-ZL3.

Queries were chosen to ensure that every library method for each
application class would be used in at least one solution, that no two
solutions would be identical, and that each solution would entail some
combination of non-trivial control-flow (e.g., pattern-matching over
type constructors) with library calls, and non-trivial synthesis of
function call arguments.

To actually define queries over these annotated libraries, we
adopted a mix of methodologies: For some benchmarks, we directly use
the verification task defined by the authors and translate it to its
synthesis dual.  For example, Figure 2 and benchmarks I10 and I11
are direct verification queries given in
<cit.>.  Similarly, the Firewall
example (D6) for deleting network devices is translated directly
from the verification queries provided in <cit.>.
Additionally, we also manually defined queries using real-life
scenarios and textbook examples, e.g. extracting read articles from
a Newsletter, while ensuring that the library protocol is followed
(D5), replacing one device with another in a firewall as a central
device (D8), etc. We also created several such real-life scenarios
for databases and textbook examples over imperative data-structure
libraries including inserting multiple elements in a hashtable,
adding elements in a queue maintaining uniqueness, etc.  For parser
examples, we relied directly upon specifications associated with
known data-dependent grammars for parsers, e.g. a PNG chunk that
must satisfy a length-payload dependence, is given as specification
query P1.

Database Benchmarks

Parsing Benchmarks

Imperative Data Structure Benchmarks

Synthesis time in seconds for  (T ) and
uni-directional approaches (Time ()) and (Time
()) and a naìve forward synthesis (Time (no-cdcl)).  The horizontal axis enumerates different synthesis

Benchmarks for which a bar does not appear for a given approach
indicate that the synthesis problem was not solvable within a 10
minute time-bound.  Graphs are given in log-scale. The ratio of size of query specification, to
the size of
synthesized expressions in terms of the number of AST nodes is given
within parentheses on the labels of the x-axis.

§.§ Results

The figures show synthesis times in seconds (the y-axis is in log
scale) executing on a standard Intel laptop with 16GB RAM.  All
queries were executed with a time-out limit of 10 mins and a bound k=5.
The timings
are for four different instantiations: the blue bar
shows timings for  (with bidirectional synthesis +
CDCL-learning); the red bar () shows
times with backward synthesis disabled, but with CDCL-leaning enabled;
c) the black bar () shows times
for just backward synthesis, with forward synthesis and CDCL disabled;
and, d) the green bar shows the synthesis time for
a naìve forward alone synthesis without the CDCL learning component.
Benchmarks with no corresponding bar indicate that the particular
instantiation could not find a solution (i.e., it either timed-out or
got stuck). Each benchmark label along the horizontal axis has an associated numeric value in parenthesis indicating the
size of the synthesized result for that query in terms of number of AST nodes, e.g. D1 (13).

§.§.§ $\textnormal{RQ}_1$ and $\textnormal{RQ}_2$: Effectiveness and impact of design decisions.

Our results show that  was successfully able to synthesize
component-based programs for all the benchmarks considered (Note: the synthesis time using for V1 (Figure  <ref>) is 1.1 seconds, hence not visible on log scale).  Overall
synthesis times for all benchmarks take less than one minute, with
approximately 32/47 completing in less than 10 seconds.  The variance
in synthesis times is primarily due to the number of quantified
variables that must be instantiated in queries supplied to Z3.  The
complexity of these generated formulae are in turn dependent on the
complexity of method specifications and synthesis queries, and the
specificity of the expected return type.  More significantly, the
chart also reveals that bi-directional synthesis can solve queries
that are not solvable using just the FW/BW-alone synthesis approaches.

Five of the benchmarks we consider (D3-D5, I7, P5) were unable to be
solved using either forward- or backward synthesis within the given
time bound.  Using just a backward synthesis ()
method fails to find solutions for 34/47 queries, while disabling
goal-directed search () fails to find a solution in
6/47 queries.  Finally, the naìve forward alone synthesis (FW-no-cdcl) was unable to find a solution for 14/47 queries.  For
the 41 queries  is able to solve,  is on
average 2x faster, justifying the benefits of our
bi-directional synthesis strategy over a unidirectional synthesis with

There are 8 queries for which FW-alone can find a solution but a
naïve synthesis without the learning component (FW-no-cdcl)
failed to find a solution. For the remaining queries where both
succeed in finding a solution, the FW-no-cdcl is on-average 6x
slower than the CDCL version, justifying the benefits of using a CDCL
mechanism as part of a forward search procedure.

Synthesized Programs
The size of synthesized programs (given in parentheses along with the
benchmark name on the x-axis) range between 6 to 38 AST nodes. These
programs include function calls, conditional control-flow,
constructors applications, etc.  The number of
components (continuous chain lengths) across synthesized programs,
range from 2 to 7, comparable to other component-based-synthesis
systems [ <cit.> (Fig. 8),  <cit.> (Table-1)].

As an example of the output  generates,
Figure <ref> presents the synthesis result for query
D11, which asks to synthesize a program that, given a globally
shared Firewall database, and two devices: d, a central device, and x, deletes d and makes x as
the central device.

The conditional branches
(lines <ref>, <ref>) distinguish cases
when we need to add x to the database before deleting d. Similarly, the nested conditional
(<ref>, <ref>) distinguishes cases when we
can directly delete d (if x is central) or when we
need to first make x a central device.

[escapechar=,basicstyle=0.9,numbers=left, breaklines=true,language=ML]
$\lambda$ (d : device) (x : device).
b1 <- is_device x;
if (b1) @@
b2 <- is_central x;
if (b2) then @@
_ <- delete_device d x;
ret ()
else @@
_ <- make_central x;
_ <- delete_device d x;
ret ()
else @@
_ <- add_device x;
_ <- make_central x;
_ <- delete_device d x;
ret ()

Synthesized Program for query the D11

Utility and Specification Efforts.
Each benchmark label along the horizontal axis also has an
associated ratio ($p$/$q$) in parenthesis, where $p$ is the size of
the query specifications in terms of the number of conjuncts in the
specification, and $q$ is the size of the synthesized result for
that query in terms of the number of AST nodes. E.g., the label D1
(5/13) implies that  given query D1, a table insertion query
whose specification has five conjuncts, produces a synthesized
program with 13 AST nodes.

These ratios highlight that for simple programs, the size of the
synthesized programs is comparable to the size of the
specifications. However, for programs with intricate control flows
found in some of the database queries (e.g., D9 and D10) or
conditional queries found in some of the imperative data structure
benchmarks (e.g., Q3 and HT2), queries are simpler because their
preconditions are weaker.  At the same time, the synthesized
programs generated are more complex, especially highlighting the
power of ś efficient enumerative search with limited

Although performs well on this traditional metric, we
found that writing such programs from scratch (even in OCaml),
without the use of libraries would typically involve non-trivial
complexity with intricate control flows, loops, recursion, etc. For
instance, in the absence of component-based synthesis support,
synthesizing a program for the query in Figure 2 would need to
synthesize code/auxiliary functions for tasks like table insertion,
checking membership, taking the average etc. This makes it
challenging to apply state-of-the-art deductive synthesis techniques
directly to our queries, given that synthesizing auxiliary functions
with these complex features in an effectful setting remains very
much an open problem <cit.>.  Thus, a more reasonable and
precise assessment of 's capabilities would involve comparing
the complexity of defining queries with the complexity of the
overall function synthesized, i.e. the combined size of the
synthesized code plus the size of each library function used in the

In summary, these results support our two main claims: (1) a
bi-directional synthesis strategy is beneficial to reason over
effectful libraries - unlike , neither  nor
could successfully discharge all the synthesis
problems in our benchmark suite; note that at least one benchmark in
each application class failed to be solved by either uni-directional
method, indicating that our technique is not specialized to a
particular application class.  And, (2) CDCL learning in this setting
is demonstrably useful - since  is also equipped with
CDCL, its execution times are competitive with  for the
benchmarks it completes.  We note that disabling CDCL in
causes at least an order of magnitude increase in
synthesis times while more than doubling the number of failing

§.§.§ $\textnormal{RQ}_3$ : Sensitivity to specification complexity and library size.

Synthesis complexity (and hence  synthesis times) is dominated by
the complexity of the queries discharged to Z3. Synthesis time
increases as function specifications and queries become more complex,
where complexity of specifications is directly correlated with the
number of uninterpreted functions and variables in the query and
number of conjuncts in propositional formulas.

Case Study

subscribe : (n : nl)-> (u :user) ->
nlmem (D , n , u) = true $\wedge$
confirmed (D, n, u) = true $\wedge$
subscribed (D, n, u) = false
v :  unit

nlmem (D', n, u) = true $\wedge$
subscribed (D', n, u) = true $\wedge$
confirmed (D', n, u) = false $\wedge$

goal : (n : nl)-> (u :user) ->

nlmem (D , n , u) = true $\wedge$
subscribed (D, n, u) = true $\wedge$
confirmed (D, n, u) = false $\wedge$
v : [string]

v = articles (D') $\wedge$ nlmem (D', n, u) = false $\wedge$

Effectful specifications for a  library
function and a synthesis query goal.  Shaded specifications
are additional properties that were added to the original to assess
the 's sensitivity to specification complexity and size.

To understand the impact of specification complexity on synthesis
capability, we compared the synthesis times for queries D1-D11 using
its provided specifications, comparing it against the synthesis times
taken when additional qualifiers are added to these specifications.
For instance, the Newsletter benchmark has three qualifiers in
its original specification viz.  nlmem (a membership
qualifier), subscribed (a Boolean-valued subscription function)
and confirmed (a Boolean-valued function, indicating if the user
has confirmed an action).  To these, we additionally include the
following four new qualifiers in a new variant of the benchmark: activenl (a Boolean-valued function that is true if a newsletter
has at least one active subscription), activeuser (a
Boolean-valued function capturing if a user has at least one active
subscription), subsize (an integer-valued function that gives
the number of newsletters a user is subscribed to) and nlreach
(the number of users which are subscribed to a newsletter).

Figure <ref> shows the specification for a
library function subscribe, which takes a newsletter n and
a user u and sets the subscription of the user for the
newsletter to true and a synthesis query (goal) to synthesize a
program which returns the list of articles read by u in n
and then unsubscribes the user from the newsletter.  The original
specification and the query is shown in black; the modified
variant includes the original formulas plus the new conjuncts (shown
in gray).
In a similar fashion we also define revised specifications for the
Firewall libraries and its associated queries (D6-D11).

Figure  <ref> shows two line graphs comparing the time
for the original run (Time (original)) compared to
the time taken to synthesize a result when these new qualifiers are

Running time comparison between original Database benchmarks against doubling the number of qualifiers in specifications.

added to specifications and queries (Time (double
qualifiers)).  Synthesis times increase from 0% to a maximum
of 26% (case D7); for most other cases, the increase is less than
20%, an indication that 's synthesis strategy scales reasonably
well against specification complexity.

§.§.§ $\textnormal{RQ}_4$ : Comparison to other enumerative
and deductive component-based synthesis techniques.

Comparison with other type-directed, component-based enumerative synthesis approaches.
To address how compares against other systems, we
consider the effectiveness of type and example-based synthesis
approaches  <cit.> in solving
effectful queries, using example demonstrations instead of
specifications to guide the synthesis procedure.  For instance,
the query,
(l : int list) $\rightarrow$ (i : int) $\rightarrow$  true  (v : int list)  size (v') = size (l) +  1

can be synthesized using type-and-examples by giving the type,
(int list $\rightarrow$ int list), and a set of input-output
examples, e.g., i) (l=[1; 2], i=3 , output=[1;2;3]) ii) (l=[1], i=1, output=[1,1]).

TYGAR <cit.> is a type-directed component-based tool that
operates over polymorphic Haskell data-types and components.  We
conducted an experiment on an extension of TYGAR, named
Hoogle+ <cit.> that allows using examples to further guide
the TYGAR synthesis process.  To perform our comparison, we modeled
the  datatype used in our running example as a
functional list over an abstract type, erasing effect annotations from
each of the libraries, and making sure to include suitable libraries
that were available in Hoogle+.

To simplify things further, we also modified the original query to
just return a new table (rather than the original  value)
as follows:
goal: (tbl : table) ->  (s : a) -> True v : table
sel (h, tbl) = Tbl $\wedge$ sel (h', tbl) = Tbl' $\wedge$ mem (Tbl', s) $\wedge$ size (Tbl') = size (Tbl) + 1;

We translated the  query above to the following Hoogle+ query:
goal : (tbl : table) -> (s : a) -> table

Running Hoogle+ on this query returns the following synthesized term:
goal = $\lambda$ (tbl : table) (s : a) . (add_tbl s)

This program is unsound given the original interface of
the add_tbl function since it can violate the uniqueness
invariant of the table, a property enforced by the library via the
precondition (not (mem (Tbl, s)) of the add_tbl function.

To refine this result, we next supplied input-output examples to
Hoogle+ to help guide it to find the required (sound) solution.  Some
of the examples provided included:

[escapechar=,basicstyle=0.9, numbers=left, breaklines=true,language=ML]
Input : tbl = [],   s = 'b' ; Output  : ['b']
Input : tbl = ['b'],   s = 'b' ; Output : ['b';'c']
Input : tbl = ['a'],   s = 'b' ; Output : ['a';'b']

[escapechar=,basicstyle=0.9, numbers=left, firstnumber=4, breaklines=true,language=ML]
Input : tbl = ['a';'c'],   s = 'b' ; Output : ['a';'c';'b']
Input : tbl = ['a';'b'],   s = 'b' ; Output : ['a';'b';'d']

Unfortunately, these examples were ineffective in helping Hoogle+ to
find a solution.  This is because, although examples are effective at capturing
structural properties like ordering, size or reformatting of inputs,
they are not very useful in defining logical cumulative properties
like membership or its negation.  The input-output pairs at lines 2-5
above try to capture such a property, but fail to do so as the
synthesizer has no way of knowing that the new elements inserted
(i.e. , ) are related to the input table by
the property not a member or are intended to be just another
character.  This example illustrates the difficulty in relating the
shape and contents of an input-output example to a provided logical
specification, especially when these specifications capture effectful

Comparison with specification-guided heap manipulating program synthesis.

A direct comparison with other heap- and
effect-aware synthesis tools <cit.> like Suslik <cit.>
or Cypress <cit.> is not feasible because of fundamental
differences in approaches and goals.  For example, Suslik supports
queries over separation-logic formulas with limited support for
component-based synthesis, and limited expressiveness to specify
effectful but non-separation specifications.  Conversely, Cobalt
defines a specification language for reasoning over components with
non-trivial effectful semantics and rich qualifiers, but does not
support separation logic formulas that capture fine-grained sharing
and aliasing properties of the heap.

These differing capabilities are in service of differing goals:
Suslik aims to synthesize recursive, pointer-manipulating programs
from inductive specifications using the shape properties expressed
in these specifications. Cobalt, on the other hand, uses pre/post
specifications of effectful libraries to guide a component-based
synthesis procedure for synthesizing non-recursive (albeit
conditional) programs for complex, effectful (albeit non-separation)
specifications that do not appeal to sophisticated shape

These differences pose major technical challenges in running
such tools on our benchmarks.  For example, in theory, our queries
correspond to non-spatial specifications in Suslik. However, both
our queries and specifications allow rich formulas with
qualifiers/method-predicates like , , etc. Unfortunately,
such specifications are beyond what is currently supported for pure
(non-spatial) formulas in Suslik, which only supports qualifiers
over a simple theory of linear arithmetic. This limitation is
discussed by the authors in follow-up work
<cit.>, Sec 4.2.

To attempt to better quantify these differences, we translated
the Cobalt synthesis problem (Sec. 3.1) to separation-logic
(spatial) formulas in Suslik because spatial formulas do allow
method predicates; each of these, however, must be given a logical
interpretation. We then ran Suslik on this translated problem.

For example, we translated the Cobalt synthesis problem given in
Figure <ref> to a Suslik query as follows.  We first
define a unique list () that is a singly-linked list with
unique elements to model the table data structure.

[escapechar=,basicstyle=0.9, breaklines=true,language=ML]
predicate ulist(loc x, set s)
| x == 0 =>  s ==  ; emp
| not (x == 0) =>  s == v ++ s1 $\wedge$ not (v in s1); [x, 2] ** x :-> v ** (x + 1) :-> nxt ** ulist(nxt, s1)

We then define two qualifiers  and
over the table as inductive separation-logic formulas:
[escapechar=,basicstyle=0.9, breaklines=true,language=ML]
predicate sll_len(loc x, int len)
| x == 0 =>  len == 0 ; emp
| not (x == 0) =>
len == len1 + 1; [x, 2] ** x :-> v **
(x + 1) :-> nxt ** sll_len(nxt, len1)

[escapechar=,basicstyle=0.9, breaklines=true,language=ML]
predicate sll_mem(loc x, int str, set s, bool mem)
| x == 0 =>  s ==         false; emp
| not (x == 0) =>
s == v ++ s1        (str == v || mem1);
[x, 2] ** x :-> v ** (x + 1) :-> nxt
** sll_mem(nxt, str, s1, mem1)

We next defined a library of functions using  and these
qualifiers in terms of separation formulas.
Finally, we took queries and translated these to Suslik
queries; for example, the functional query specification shown in
Figure <ref> can be written as follows:
[escapechar=,basicstyle=0.9,  breaklines=true,language=ML]
void goal (loc r, loc ret)
r :-> x ** ret :-> val ** ulist (x, s) ** sll_len (x, n)
(mem == true) $\wedge$ n1 == n + 1; r :-> y ** ulist (y, s1) ** sll_mem (y, val, s1, mem) ** sll_len (y, n1)

A formula in Suslik has two components { $\phi$; $P$}; a non-separation formula (authors call it a pure formula) $\phi$ and an impure component $P$ possibly containing separation formulas. $P$ contains points-to specification (written as x :-> y) and separating conjuncts (written as ($P1$ ** $P2$)).
The above query's post-condition thus requires that the size of the output ulist (represented by y), which is pointed-to by r, has size one greater than the input ulist (represented by x), and the returned value (represented by val) is present in y.

Benchmark     Cobalt     Suslik

I1     $\checkmark$     err

I4     $\checkmark$     t/o

I5     $\checkmark$     t/o

I6     $\checkmark$     err

I9     $\checkmark$     t/o

I10     $\checkmark$     t/o

I11     $\checkmark$     t/o

V1     $\checkmark$     err

Results of running selected Cobalt queries on Suslik.

On this query, the tool timed out with a timeout of 30000
seconds[This is the timeout value set in the online version
of the tool.]  (approx.  8 hours 20 minutes).  We ran a similar
experiment on several other benchmarks wherever it was
possible for us to define an inductive separation-logic predicate
corresponding to the qualifiers in our specifications for the
data-structure used in the benchmarks. Figure <ref> shows
the results for these benchmakrs. For each of these experiments,
Suslik either timed-out (t/o) or generated a program with an error expression, a result indicating an inconsistent internal
state encountered while solving the query.

These experiments give anecdotal evidence about our claim of
differing capabilities and goals.  We conjecture the timeout happens
because Suslik hides complexities of the function call rule into a
call-abduction routine. This routine prepares the current heap (say
) to take it to another heap (say ) such that
the precondition of a function  holds in
. Thus, Suslik uses an abduction (forward search)
procedure for resolving multiple function calls.  While this may be
sufficient in the case of a single recursive function call, its
generalization to handle multiple library functions requires a
multi-abduction decision procedure <cit.> to
resolve, a challenging problem in the presence of expressive
data structures of the kind used in our benchmarks <cit.>.

§.§ Limitations

relies on automated verification of the programs for its
forward, backward as well as the CDCL search procedures.  This
reliance requires to make fundamental assumptions about
library behavior that (a) each heap object (OCaml reference) is
always referenced by a unique path (e.g, a variable  or a
field access ) and, (b) that there is no sharing of
heap objects. This allows us to reason locally and automatically
about effectful behavior of library functions without the need for
reasoning over separation-logic formulas.  In practice, this
restriction prevents us from synthesizing programs fron libraries
that do require heap sharing, for example, those that implement
cyclic data structures, graphs, etc.  We leave incorporating
approaches such as <cit.> that enable some
degree of automated verification for programs specified using
separation formulas into our synthesis pipeline as a topic for
future work.

§ RELATED WORK

Deductive Program Synthesis.  Closely related
deductive synthesis approaches to ours include Suslik <cit.>
and its follow-up work Cypress <cit.>, both of which take
Hoare-triple style specifications and have synthesis rules for
function calls.  An important difference between and Suslik
specifications stems from the form of Suslik pre- and post-conditions,
{$\phi$; P} $\rightarrow$ {$\phi'$ ; Q}, that are expressed using
two components - a non-separation part $\phi$ defining constraints on
the logical data structure associated with the actual mutable data
structure, and a spatial part defining assertions related to the
shape of the heap.  The pre- and post-formulas in specifications
are analogous to the non-separation part of Suslik specifications; our
specification framework has no corresponding analog to Suslik's
spatial component.  For non-spatial properties, however, our queries,
and consequently our specifications, enable rich formulas with
qualifiers, expressivity that is beyond what is currently supported
for pure formulas in Suslik, which only supports a simple theory of
linear arithmetic.
These significant differences lead to fundamentally different
synthesis strategies making any kind of direct comparison infeasible.
We note that Suslik does allows libraries of functions through their (Abduce Call) rule
which is a naìve call-abduction routine that is equivalent to 's no-cdcl
approach in theory.

Other deductive synthesis <cit.> and
proof-search guided synthesis efforts <cit.> use
deductive proof rules for synthesizing pure terms.  In contrast, our
synthesis rules operate over heap manipulating expressions (viz.
effectful function calls and sequencing).  Synquid <cit.> uses
a bi-directional typing calculus to synthesize functional
programs. However their notion of bi-directionality is related to
bi-directional typing <cit.>, which is unrelated to the
notion of bi-directionality used in  that is defined with
respect to forward and backward proof search over programs with
effectful specifications <cit.>.  Viser <cit.>
uses a light-weight bidirectional abstract interpretation coupled
tightly to table transformation tasks that can reason specifically
about simple table inclusion constraints; however, it cannot handle
general effectful specifications of the kind intended to be used in

Component-based Synthesis and Learning.  There
is a long line of work on the use of component-based synthesis in the
context of domain-specific languages <cit.> as well as general-purpose programming
domains <cit.>.
is distinguished from these other systems in the form of the
query specifications that we consider (formal query specifications
expressed as Hoare triples vs.  input-output or informal
specifications as found in <cit.>);
and, in our expectation that the libraries from which synthesized
programs are constructed are effectful, in contrast to the assumptions
made in <cit.>. Although Sypet <cit.> does
support effectful libraries, it does not use library protocol
specifications to guide synthesis and consequently cannot enforce
associated library protocols or programs that require conditional

Our CDCL-learning based enumeration is similar in spirit to the
conflict-driven learning based synthesis of pure
components <cit.>, and is inspired by conflict-driven
learning based enumeration techniques found in modern SAT
solvers <cit.>.  The discriminating propositions learned in
, however, must include the path-sensitive, effectful semantics
of failed programs in terms of the strongest postconditions associated
with these programs, in contrast to the simpler, global set of Boolean
propositional formulas associated with the partial failed programs
found in  <cit.>, such a global formula in presence of effectful libraries
with path-sensitive information will grow too large and overwhelm the solver.
Further, we must also account for
program failures due to bounded exploration of an unbounded search
space without losing completeness, a challenge  <cit.>
does not face.

§ CONCLUSIONS

We present a new specification-guided synthesis framework capable of
synthesizing effectful programs from a library of effectful
components.  We capture the behavior of these components using a rich
specification language that capture effectful behavior in terms of
Hoare-style pre- and post-conditions.  The synthesis procedure itself
combines forward and backward proof search with respect to these
specifications, integrating a CDCL-style learning framework to enable
scalability.  Experimental results on a tool () that integrates
these ideas are promising, demonstrating 's ability to
efficiently synthesize programs over complex effectful queries,
guaranteed to be consistent with component specifications.

We thank the anonymous reviewers for their detailed comments and
suggestions.  Funding for this work material is supported in part by
DARPA, under the Safe Documents (SafeDocs) program.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Appel, Beringer, and CaoAppel
et al2021]
authorpersonAndrew Appel, personLennart
Beringer, and personQinxiang Cao.
booktitle. seriesSoftware Foundations,
Vol. volume5.
publisherElectronic textbook, Chapter Verifiable C.
Version 1.1.1, .

[Biere, Heule, van Maaren, and WalshBiere
et al2009]
editorpersonArmin Biere, personMarijn
Heule, personHans van Maaren, and personToby
Walsh (Eds.). year2009.
booktitleHandbook of Satisfiability.
seriesFrontiers in Artificial Intelligence and Applications,
Vol. volume185. publisherIOS Press.

[Charguéraud, Filliâtre, Pereira, and
PottierCharguéraud et al2017]
authorpersonArthur Charguéraud,
personJean-Christophe Filliâtre, personMário
Pereira, and personFrançois Pottier.
titleVOCAL – A Verified OCaml Library.
howpublishedML Family Workshop.

[de Moura and Bjørnerde Moura and
authorpersonLeonardo de Moura and
personNikolaj Bjørner. year2008.
Z3: An Efficient SMT Solver. In
booktitleTools and Algorithms for the Construction and
Analysis of Systems, editorpersonC. R. Ramakrishnan
and personJakob Rehof (Eds.). publisherSpringer
Berlin Heidelberg, addressBerlin, Heidelberg,

[Delaware, Pit-Claudel, Gross, and
ChlipalaDelaware et al2015]
authorpersonBenjamin Delaware,
personClément Pit-Claudel, personJason Gross,
and personAdam Chlipala. year2015.
Fiat: Deductive Synthesis of Abstract Data Types in
a Proof Assistant. In booktitleProceedings of the 42nd
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(Mumbai, India) (seriesPOPL '15).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages689–700.

[Delaware, Suriyakarn, Pit-Claudel, Ye, and
ChlipalaDelaware et al2019]
authorpersonBenjamin Delaware, personSorawit
Suriyakarn, personClément Pit-Claudel,
personQianchuan Ye, and personAdam Chlipala.
Narcissus: Correct-by-Construction Derivation of
Decoders and Encoders from Binary Formats.
journalProc. ACM Program. Lang.
volume3, numberICFP, Article articleno82
(dateJuly year2019), numpages29 pages.

[Dunfield and KrishnaswamiDunfield and
authorpersonJana Dunfield and personNeel
Krishnaswami. year2021.
Bidirectional Typing.
journalACM Comput. Surv. volume54,
number5, Article articleno98 (datemay
year2021), numpages38 pages.

[Feng, Martins, Bastani, and DilligFeng
et al2018]
authorpersonYu Feng, personRuben Martins,
personOsbert Bastani, and personIsil Dillig.
Program Synthesis Using Conflict-Driven Learning.
In booktitleProceedings of the 39th ACM SIGPLAN Conference
on Programming Language Design and Implementation (Philadelphia, PA, USA)
(seriesPLDI 2018). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Feng, Martins, Van Geffen, Dillig, and
ChaudhuriFeng et al2017a]
authorpersonYu Feng, personRuben Martins,
personJacob Van Geffen, personIsil Dillig, and
personSwarat Chaudhuri. year2017a.
Component-Based Synthesis of Table Consolidation
and Transformation Tasks from Examples. In
booktitleProceedings of the 38th ACM SIGPLAN Conference on
Programming Language Design and Implementation (Barcelona, Spain)
(seriesPLDI 2017). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Feng, Martins, Wang, Dillig, and RepsFeng
et al2017b]
authorpersonYu Feng, personRuben Martins,
personYuepeng Wang, personIsil Dillig, and
personThomas W. Reps. year2017b.
Component-Based Synthesis for Complex APIs. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages (Paris, France)
(seriesPOPL 2017). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Frankle, Osera, Walker, and ZdancewicFrankle
et al2016]
authorpersonJonathan Frankle,
personPeter-Michael Osera, personDavid Walker, and
personSteve Zdancewic. year2016.
Example-Directed Synthesis: A Type-Theoretic
Interpretation. In booktitleProceedings of the 43rd Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St.
Petersburg, FL, USA) (seriesPOPL '16).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages802–815.

[Ganzinger, Hagen, Nieuwenhuis, Oliveras, and
TinelliGanzinger et al2004]
authorpersonHarald Ganzinger, personGeorge
Hagen, personRobert Nieuwenhuis, personAlbert
Oliveras, and personCesare Tinelli.
DPLL(T): Fast Decision Procedures. In
booktitleComputer Aided Verification,
editorpersonRajeev Alur and
personDoron A. Peled (Eds.). publisherSpringer Berlin
Heidelberg, addressBerlin, Heidelberg,

[Guo, James, Justo, Zhou, Wang, Jhala, and
PolikarpovaGuo et al2019]
authorpersonZheng Guo, personMichael James,
personDavid Justo, personJiaxiao Zhou,
personZiteng Wang, personRanjit Jhala, and
personNadia Polikarpova. year2019.
Program Synthesis by Type-Guided Abstraction
journalProc. ACM Program. Lang.
volume4, numberPOPL, Article articleno12
(dateDec. year2019), numpages28 pages.

[Guria, Foster, and Van HornGuria
et al2021]
authorpersonSankha Narayan Guria,
personJeffrey S. Foster, and personDavid Van Horn.
RbSyn: Type- and Effect-Guided Program Synthesis.
In booktitleProceedings of the 42nd ACM SIGPLAN
International Conference on Programming Language Design and Implementation
(Virtual, Canada) (seriesPLDI 2021).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages344–358.

[Itzhaky, Kotek, Rinetzky, Sagiv, Tamir, Veith,
and ZulegerItzhaky et al2017]
authorpersonShachar Itzhaky, personTomer
Kotek, personNoam Rinetzky, personMooly Sagiv,
personOrr Tamir, personHelmut Veith, and
personFlorian Zuleger. year2017.
On the Automated Verification of Web Applications
with Embedded SQL. In booktitle20th International
Conference on Database Theory, ICDT 2017, March 21-24, 2017, Venice,
Italy (seriesLIPIcs, Vol. volume68),
editorpersonMichael Benedikt and
personGiorgio Orsi (Eds.). publisherSchloss Dagstuhl
- Leibniz-Zentrum für Informatik, pages16:1–16:18.

[Itzhaky, Peleg, Polikarpova, Rowe, and
SergeyItzhaky et al2021]
authorpersonShachar Itzhaky, personHila
Peleg, personNadia Polikarpova, personReuben N. S.
Rowe, and personIlya Sergey. year2021.
Cyclic Program Synthesis. In
booktitleProceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation (Virtual,
Canada) (seriesPLDI 2021). publisherAssociation
for Computing Machinery, addressNew York, NY, USA,

[James, Guo, Wang, Doshi, Peleg, Jhala, and
PolikarpovaJames et al2020a]
authorpersonMichael B. James, personZheng
Guo, personZiteng Wang, personShivani Doshi,
personHila Peleg, personRanjit Jhala, and
personNadia Polikarpova. year2020a.
Digging for Fold: Synthesis-Aided API Discovery
for Haskell.
journalProc. ACM Program. Lang.
volume4, numberOOPSLA, Article
articleno205 (datenov year2020),
numpages27 pages.

[James, Guo, Wang, Doshi, Peleg, Jhala, and
PolikarpovaJames et al2020b]
authorpersonMichael B. James, personZheng
Guo, personZiteng Wang, personShivani Doshi,
personHila Peleg, personRanjit Jhala, and
personNadia Polikarpova. year2020b.
Digging for Fold: Synthesis-Aided API Discovery for
journalProc. ACM Program. Lang.
volume4, numberOOPSLA, Article
articleno205 (datenov year2020),
numpages27 pages.

[Jha, Gulwani, Seshia, and TiwariJha
et al2010]
authorpersonSusmit Jha, personSumit
Gulwani, personSanjit A. Seshia, and personAshish
Tiwari. year2010.
Oracle-Guided Component-Based Program Synthesis.
In booktitleProceedings of the 32nd ACM/IEEE International
Conference on Software Engineering - Volume 1 (Cape Town, South Africa)
(seriesICSE '10). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Jim, Mandelbaum, and WalkerJim
et al2010]
authorpersonTrevor Jim, personYitzhak
Mandelbaum, and personDavid Walker.
Semantics and Algorithms for Data-Dependent
Grammars. In booktitleProceedings of the 37th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Madrid,
Spain) (seriesPOPL '10). publisherAssociation
for Computing Machinery, addressNew York, NY, USA,

[Kneuss, Kuraj, Kuncak, and SuterKneuss
et al2013]
authorpersonEtienne Kneuss, personIvan
Kuraj, personViktor Kuncak, and personPhilippe
Suter. year2013.
Synthesis modulo Recursive Functions. In
booktitleProceedings of the 2013 ACM SIGPLAN International
Conference on Object Oriented Programming Systems Languages and
Applications (Indianapolis, Indiana, USA) (seriesOOPSLA
'13). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages407–426.

authorpersonJ. McCarthy.
booktitleTowards a Mathematical Science of
publisherSpringer Netherlands,
addressDordrecht, pages35–56.

[Nanevski, Morrisett, and BirkedalNanevski
et al2006]
authorpersonAleksandar Nanevski, personGreg
Morrisett, and personLars Birkedal.
Polymorphism and Separation in Hoare Type
(year2006), pages62–73.

[Nanevski, Morrisett, Shinnar, Govereau, and
BirkedalNanevski et al2008]
authorpersonAleksandar Nanevski, personGreg
Morrisett, personAvraham Shinnar, personPaul
Govereau, and personLars Birkedal.
Ynot: Dependent Types for Imperative Programs.
In booktitleProceedings of the 13th ACM SIGPLAN
International Conference on Functional Programming (Victoria, BC, Canada)
(seriesICFP '08). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

ocaml year[n.d.].
titleParsing with Ocamllex.

[Osera and ZdancewicOsera and
authorpersonPeter-Michael Osera and
personSteve Zdancewic. year2015.
Type-and-Example-Directed Program Synthesis. In
booktitleProceedings of the 36th ACM SIGPLAN Conference on
Programming Language Design and Implementation (Portland, OR, USA)
(seriesPLDI '15). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Polikarpova, Kuraj, and
Solar-LezamaPolikarpova et al2016]
authorpersonNadia Polikarpova, personIvan
Kuraj, and personArmando Solar-Lezama.
Program Synthesis from Polymorphic Refinement
Types. In booktitleProceedings of the 37th ACM SIGPLAN
Conference on Programming Language Design and Implementation (Santa
Barbara, CA, USA) (seriesPLDI '16).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages522–538.

[Polikarpova and SergeyPolikarpova and
authorpersonNadia Polikarpova and
personIlya Sergey. year2019.
Structuring the Synthesis of Heap-Manipulating
journalProc. ACM Program. Lang.
volume3, numberPOPL, Article articleno72
(dateJan. year2019), numpages30 pages.

authorpersonJ. C. Reynolds.
Separation logic: a logic for shared mutable data
structures. In booktitleProceedings 17th Annual IEEE
Symposium on Logic in Computer Science. pages55–74.

[Sekiyama and IgarashiSekiyama and
authorpersonTaro Sekiyama and
personAtsushi Igarashi. year2017.
Stateful Manifest Contracts. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages (Paris, France)
(seriesPOPL 2017). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Shi, Steinhardt, and LiangShi
et al2019]
authorpersonKensen Shi, personJacob
Steinhardt, and personPercy Liang.
FrAngel: Component-Based Synthesis with Control
journalProc. ACM Program. Lang.
volume3, numberPOPL, Article articleno73
(datejan year2019), numpages29 pages.

[Swamy, Weinberger, Schlesinger, Chen, and
LivshitsSwamy et al2013]
authorpersonNikhil Swamy, personJoel
Weinberger, personCole Schlesinger, personJuan Chen,
and personBenjamin Livshits. year2013.
Verifying Higher-Order Programs with the Dijkstra
Monad. In booktitleProceedings of the 34th ACM SIGPLAN
Conference on Programming Language Design and Implementation (Seattle,
Washington, USA) (seriesPLDI '13).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages387–398.

[Wadler and ThiemannWadler and
authorpersonPhilip Wadler and personPeter
Thiemann. year2003.
The Marriage of Effects and Monads.
journalACM Trans. Comput. Logic
volume4, number1 (dateJan.
year2003), pages1–32.

[Wang, Feng, Bodik, Cheung, and DilligWang
et al2019]
authorpersonChenglong Wang, personYu Feng,
personRastislav Bodik, personAlvin Cheung, and
personIsil Dillig. year2019.
Visualization by Example.
journalProc. ACM Program. Lang.
volume4, numberPOPL, Article articleno49
(datedec year2019), numpages28 pages.

[Zhang, Madigan, Moskewicz, and MalikZhang
et al2001]
authorpersonLintao Zhang, personConor F.
Madigan, personMatthew H. Moskewicz, and
personSharad Malik. year2001.
Efficient Conflict Driven Learning in a Boolean
Satisfiability Solver. In booktitleProceedings of the 2001
IEEE/ACM International Conference on Computer-Aided Design (San Jose,
California) (seriesICCAD '01). publisherIEEE
Press, pages279–285.

§ SUPPLEMENTAL MATERIAL FOR THE MAIN PAPER

§.§ Extended Forward Synthesis Rules

$\Gamma  \ottsym{;}  \Sigma
\vdash  \tau  \twoheadrightarrow  \ottnt{e}$
Forward Synthesis

[FW_ConsApp]Γ; Σ⊢τ_j ↠y_j

D_i (x_j: τ_j) →{ν: TN | ϕ_i} ∈Σ

ϕ_i[y_j/x_j] => ϕ_i'
Γ;Σ⊢{ν: TN | ϕ_i'} ↠D_i (y_j)

[FW_Ref]  l : t  ref ∈Γ
Γ;Σ⊢t  ref  ↠l

[FW_Lambda]Γ, x_i : τ_i; Σ⊢τ↠e
Γ;Σ⊢(x_i : τ_i) →τ↠λ(x_i :τ_i). e

Extra FW_Synthesis Rules

§.§ Typing Rules for $\lambda_{\mathit{eff}}$

Fig. <ref> presents typing semantics for $L$-expressions. Each typing judgment is of the
$\Gamma;\Sigma \vdash$ e  : $\tau$, saying, in a environment $\Gamma;\Sigma$, an expression $e$ has a
type $\tau$.

[T-var]x : τ∈Γ

Γ; Σ⊢x : τ

[T-consapp] D_i (x_j: τ_j) →{ν: TN | ϕ_i} ∈Σ

Γ; Σ⊢x_i : τ_i
Γ; Σ⊢D_i (y_j) : {ν: TN | {ϕ_i [y_i/x_i]}

[T-call] Γ; Σ⊢f : (x_i : τ_i) →{P} v : t {Q}

Γ; Σ⊢y_i : τ_i

Γ; Σ⊢f (y_i) : {P[y_i/x_i]} v : t { Q[y_i/x_i]}

D_i (x_j: τ_j) →{ν: TN | ϕ} ∈Σ

Γ;Σ⊢e : {ν: TN | ϕ}

Γ, x_j : τ_j; Σ⊢e_i : τ
Γ; Σ⊢match  e  with   D_i (x_j) -> e_i : τ

[T-if] Γ;Σ⊢e : { ν: bool | ϕ_t ∧ϕ_f}

Γ, ϕ_t[true/ν];Σ⊢e_t : τ

Γ, ϕ_f[false/ν];Σ⊢e_f : τ
Γ; Σ⊢if  e  then   e_t  else  e_f : τ

[T-frame] Γ;Σ⊢e : {P} ν: t {Q}

(  (  Vars   (  R
)  )   ∩  (  EVars   (
P     ,  Q     )  )  )
=    ∅
(  (  Qual   (  R
)  )   ∩

(  (  Qual
(  P     )  )   ∪  (
Qual   (  Q     )  )  )
)   =   (  ∅)

Γ;  Σ⊢e :  {  P     ∧(  R     )  }  ν:  t
{  Q     ∧(  R     )

[T-seq] Γ; Σ⊢e_1 : {P1 } ν: t_1 { Q1}

Γ, x : t_2 ⊢e_2 : {P2 } ν: t_2 {Q2}

Γ; Σ⊢{P1 ∧Q1 => P2} ν: t2 {Q1 ∧Q2 }

[T-sub]Γ; Σ⊢e : {P1} ν: t {Q1}

Γ; Σ⊢P => P1      Γ; Σ⊢Q1 => Q

Γ; Σ⊢e : {P} ν: t {Q}

Γ; Σ⊢((??) : τ) : τ

Γ; Σ⊢skip : {True} v : unit {True}

Typing Rules for $\lambda_{\mathit{eff}}$ expressions

§ DETAILS OF SOUNDNESS THEOREMS AND PROOFS

§.§ Soundness

If $\Gamma  ;  \Sigma  \vdash  \{ \phi_{{\mathrm{1}}} \}  \diamondsuit  \{
\phi_{{\mathrm{2}}}  \} \twoheadleftarrow \ottnt{e}$ or
$\Gamma  \ottsym{;}  \Sigma  \vdash  \tau  \twoheadleftarrow  \ottnt{e}$ then
$\Gamma$;$\Sigma$ $\vdash$ e : $\{ \phi_{{\mathrm{1}}} \}  v : t  \{
\phi_{{\mathrm{2}}}  \}$ or $\Gamma$;$\Sigma$ $\vdash$ e : $\tau$ respectively.

The proof is via induction over BW_Synthesis rules (Figure 8 in the main paper):
First, the bases cases:

* Case BW_FW : Using Lemma  <ref>

* Case BW_Hole : Using Typing rule for hole (T-hole) (refer Figure <ref>) and typing rule
for sequencing (T-seq) for the term y $\leftarrow$ (??) : $\tau$ ; skip.

Next the inductive cases:

* Case BW_Call : We give a proof for a function call with 1 argument, the general case will be an
inductive argument over number of arguments i:

* Using IH $\Gamma; \Sigma$ $\vdash$ $y_i$ : $\tau_i$ and $\Gamma; \Sigma$ $\vdash$ $e_i$ : { P} (??) :
$\tau_i$ {P'}.

* Using Typing rule for function application (T-call), the type for the function
call f ($y_i$) for the given post condition Q is given by {P1 $\wedge$ (Q1 $\implies$ Q)} v : t' {Q}.
Which is equivalent to { P' } v:t' {Q} using the definition of P'.

* Using the typing rule for sequencing for the sequence term ($y_i$ $\leftarrow$ $e_i$; f ($y_i$)) we get
{P} v : t' {P' $\wedge$ Q}.

* Using 1-3 and the subtyping rule for effectful computations, T-sub, we get $\Gamma; \Sigma$ $\vdash$ e
: {P} v : t' {Q}.

* Case BW_Frame :

* Using IH over the premise we get $\Gamma; \Sigma$ $\vdash$ e : {$P_1$} (??) : t {$Q_1$}.

* Using the T-frame rule and the constraints in the premise viz. (P $\vdash$ $P_1$ $\wedge$ $R$),
($Q_1$ $\wedge$ $R$ $\vdash$ Q), we get the goal condition.

* Case BW_Sub : Using IH and subtyping rule for computations (T-sub).

If $\Gamma  \ottsym{;}  \Sigma  \vdash  \tau  \twoheadrightarrow  \ottnt{e}$ then
$\Gamma$;$\Sigma$ $\vdash$ e : $\tau$.

The proof methodology is similar to the BW-Soundness, but is defined over the FW_Synthesis rules

Applying Induction on the Forward Synthesis rules:
(Figure 7 in the main-paper and Figure <ref> in this Supplemental material for extended rules) and
the typing rules for $\lambda_{\mathit{eff}}$ expressions (Figure <ref>).
First the base cases :

* Case FW_Var : Directly using the T-var rule.

* Case FW_Ref : Using the T-ref rule.

Next the inductive Cases:

* Case FW_ConsApp : Using IH, $\Gamma;\Sigma$ $\vdash$ $y_i$ : $\tau_i$ and using the T-consapp rule, we
get $\Gamma;\Sigma$ $\vdash$ $D_i$ ($\overline{y_i}$) : {v : TN | $\phi_i'$}.

* Case FW_Lambda : Using IH and T-lambda rule.

* Case FW_Match : Using IH and T-match rule.

* Case FW_If : Using IH on the two branches and combining the results using the T-if rule.

* Case FW_Call : The proof again is for function call with 1 argument, the general case will be an
inductive argument over the number of arguments i:

* Using IH $\Gamma; \Sigma$ $\vdash$ $y_i$ : $\tau_i$.

* Using Typing rule for function application (T-call), the type for the function
call f ($y_i$) for the given post condition Q is given by {P  $\wedge$ (P $\implies$ P1)} v : t' {P
$\wedge$ Q1}.
Which is equivalent to { P } v:t' {Q'} using the definition of Q'.

* Using IH, $\Gamma; \Sigma$ $\vdash$ $e$ : { Q'} v : t Q.

* Using the typing rule for sequencing for the sequence term (f ($y_i$);$z$ $\leftarrow$ $e$; ) we get
{P} v : t' {Q' $\wedge$ Q}.

* Using 1-3 and the subtyping rule for effectful computations, T-sub, we get $\Gamma; \Sigma$ $\vdash$ e
: {P} v : t' {Q}.

* Case FW_Frame : Using IH over the premise we get $\Gamma; \Sigma$ $\vdash$ {$P$} v:t {$Q$}. Using
the T-frame rule we get the goal condition.

* Case FW_Sub : Using IH and the T-Sub rule for computation Subtyping.

Iff Synthesize ($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\varnothing$) = e then
$\Gamma$;$\Sigma$ $\vdash$ e : $\tau$.

The proof of the soundness theorem is by a case analysis over the Synthesize routine followed by an
induction on forward/backward synthesis rules, while using $\lambda_{\mathit{eff}}$ typing semantics.

From the premise of the Soundness statements : Given Synthesize ($\langle\Gamma$,$\Sigma$,
$\Psi\rangle$, $\varnothing$) = e.
Performing a case-split over , when Synthesize return an e $\neq$ $\bot$ we get the following cases: We
first take the simpler of the two cases:

* The if case, (line 3, Algorithm 1 in main-paper): e = BW_Rules ($\Gamma, \Sigma, \Psi$, F)
We get this directly using the Lemma <ref>.

* The else case, (line 7 Algorithm 1):  e = $e_f$ ; $e_b$, where
$e_f$ = CDCL ($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\mathtt{H}$) and $e_b$ = BW_Rules
($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\mathtt{F}$).

* Using the definition of CDCL, iff e = CDCL ($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\mathtt{H}$) then
e = FW_SUB ($\Gamma$,$\Sigma$, ($p_i$),  $\Psi\rangle$) (line 19, Algorithm 1).

* Further, using the soundness result for forward synthesis rules (Lemma <ref>, we get
$\Gamma;\Sigma$ $\vdash$ $e_f$ : $\Psi$.

* $\Psi'$ is defined as {P} v : _ {WP ($e_b$, Q)}

* Using a-c and T-seq, the type for e = $e_f$; $e_b$ is {P} v : t {Q}.

§.§ Completeness

Since the CDCL routine (refer Algorithm 1) can possibly discard a correct program if
it can ensure that there exists another program satisfying the given query-spec, the completeness
argument is relative to a query spec.

$\forall$ k. If Synthesize ($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\varnothing$) =  $\bot$
then $\nexists$ e. $\mid$ e $\mid$ $\leq$ k and $\Gamma$; $\Sigma$ $\vdash$ e : $\Psi$.

For a given value of k, let us call the original search space of programs of size less than or equal to k
as $S_k$. The CDCL search strategy is exhaustive over the search-space it maintains while filtering out
k-equivalent-modulo-stuckness program terms, let us call this filtered search space as ${S_{k}}^{\Psi}$ thus,
the only source of incompleteness leading to the failure of the above theorem can occur iff there exists a term
e in the original unfiltered search space (e $\in$ $S_{k}$) such that $\Gamma; \Sigma$ $\vdash$ e : $\Psi$,
but e $\notin$ ${S_{k}}^{\Psi}$ and $\nexists$ e' $\in$  ${S_{k}}^{\Psi}$, such that $\Gamma; \Sigma$ $\vdash$
e' : $\Psi$. Our completeness proof argues that this condition can never occur in CDCL.

We define a small-subset relation between two search-spaces $S_k$ and
${S_k}^{\Psi}$ for programs of size upto $k$ and a given  synthesis
problem $\Psi$, such that if ${S_k}^{\Psi}$ is a small-subset of $S_k$,
then a) it is a subset of $S_k$ and b) iff there exists a solution for the
synthesis problem $\Psi$ in $S_k$ then there must exists a solution to the
problem in ${S_k}^{\Psi}$.

A search space $S_k$ is a finite set of all possible expressions ${\mid e
\mid}_{k}$ of length upto k. A   small-subset ${S_{k}}^{\Psi}$
$\subseteq$ $S_k$ is a search space such that if $\exists$ $e$ $\in$ $S_k$ ,
such that $\Gamma$; $\Sigma$ $\vdash$ $e$ : $\Psi$, then $\exists$ $e'$ $\in$
${S_{k}}^{\Psi}$ with $e'$ possibly same as $e$ and $\Gamma$; $\Sigma$ $\vdash$
$e'$ : $\Psi$.

For a given k and $\Psi$ $\equiv$ {$\phi$} v : t { $\phi'$}, a path $p_i$ $\equiv$ $c_1;c_2;...c_i$ is a
k-bound-stuck-path if either of the following two conditions hold :

* $\nexists$ $c_{i+1}$ such that SP ($\phi$, $p_i$) => $Pre_{c_{i+1}}$, where $Pre_{c_{i+1}}$ is the
preconditions for the Specification of $c_{i+1}$.

* i = k-1 and $\forall$ $c_k$. (SP ($\phi$, $p_i$) => $Pre_{c_{k}}$) => ($\neg$ (SP ($\phi$, $p_i;c_k$) =>

$\forall$ k. the CDCL-Search (Algorithm 1, main-paper) always maintains a Small-subset of the
search space $S_k$.

Let $\Psi$ $\equiv$ {$\phi$} v : t {$\phi'$}, since the CDCL algorithm works at an abstraction of paths,
we defined e as a path, i.e. a sequence of
components. e $\equiv$ $c_1;c_2;....c_i;...c_m$.

Given, e $\in$ $S_k$ and $\Gamma; \Sigma$ $\vdash$ e: $\Psi$ and  e $\notin$ ${S_k}^{\Psi}$.
we get  $c_1;c_2;....c_i;...c_m$ $\notin$ ${S_k}^{\Psi}$. This can only occur if the path was filtered by CDCL
at some i between 1..m.  Thus without the loss of generality we can pick one such component say $c_j$,
j $\in$ [1, m-1], such that $p_j$ $\equiv$ $c_1;...c_j$ $\in$ ${S_k}^{\Psi}$ and $p_{j+1}$
$\equiv$ $c_1;...c_j;c_{j+1}$ $\notin$ ${S_k}^{\Psi}$.
For this to occur, the $\mathcal{R}_{Choice}$ (..., $p_j$) (line 13, Algorithm 1 in the main paper) must not
return $c_{j+1}$.
Internally, $\mathcal{R}_{Choice}$ skips a component $c_{j+1}$ iff the following fails:
($H; D ; \Gamma; \Sigma;  \vdash  (\Psi, p_j) \hookrightarrow (p_j;c_{j+1})$)
Following the rule CDCL_CHOICE (Figure 9, main-paper), this can happen in the following cases:

* $\mid$ $p_j;c_{j+1}$ $\mid$ > k : However, from the definition of e, $p_j$ and the premise of the
Lemma, $\mid$ c $\mid$ $\leq$ k, and hence $\mid$ $p_j;c_{j+1}$ $\mid$ $\leq$ k, thus this case never occurs.

* $\neg$ (($p_j;c_{j+1}$) $\prec$ $H$ : By the definition of $\prec$, if $\neg$ (($p_j;c_{j+1}$)
$\prec$ $H$, then $\neg$ (e $\prec$ $H$), however this contradicts our premise that $\Gamma; \Sigma$ $\vdash$
e : $\Psi$. Thus the only allowed cases is the following:

* $\neg$ [$\Gamma$] $\models$ X : This is the only case which is possible:

Using (3), $\neg$ [$\Gamma$] $\models$ X $\implies$ the following two propositions:

* Conjunct #1 in X is false, i.e. ($\phi_s => \mathbf{SP (\phi, (p_j;c_{j+1})}$) :
Using the definition of $\phi_s$ from rule CDCL_LEARN, (Figure 9, main-paper) and the definition of
k-stuck-node (Definition <ref>), we can do the following case-split:

* For all stuck paths, $p_{stuck}$, $\nexists$ $c_l$ $\in$ $\Sigma$, such that SP ($\phi$,
$p_{stuck}$ => $Pre_{c_l}$), thus the failing proposition ($\phi_s$ => $\mathbf{SP (\phi, (p_j;c_{j+1})}$)
implies that
$\nexists$ $c_l$ $\in$ $\Sigma$, such that  ($\mathbf{SP (\phi, (p_j;c_{j+1})}$ => $Pre_{c_l}$), thus
$(p_j;c_{j+1})$ is a stuck path, this violates our definition of e as a solution.

* We are left with the case when, $\mid$ $p_{stuck}$ $\mid$ = k-1 and $\forall$ $c_l$. SP ($\phi$,
$p_{stuck}$ => $Pre_{c_l}$) => $\neq$ SP ($\phi$, $p_{stuck};c_l$ => $\phi'$). The failure of second
proposition in X, handles this case:

* Conjunct #2 in X is false, i.e.
$\neg$ $\{(\mathbf{SP (\phi, (p_j;c_{j+1}))} => \phi_t) \wedge \neg
(\mathbf{SP (\phi, (p_j))} => \phi_t)\}$ :
For the premise of the lemma to be true, i.e. e $\equiv$ $c_1;c_2;...c_j;..c_m$ $\in$ $S_k$ and
$\Gamma; \Sigma$ $\vdash$ e: $\Psi$, it must be the case that ($\mathbf{SP (\phi, (p_j;c_{j+1})}$) =>
$Pre_{c_{j+2}}$, thus, $c_{j+1}$ must be one of the truncated components:
Using the definition of $\phi_t$ from rule CDCL_LEARN (Figure 9, main-paper), Conjunct #2, we can
conclude, iff ($\mathbf{SP (\phi, (p_j;c_{j+1};c_{j+2};..c_m)}$) => {$\phi'$}, then we have a smaller term
e' = $p_j;c_{j+2};..c_m$,
such that (SP($\phi$, e')) => {$\phi'$}.

$\forall$ k. If Synthesize ($\langle\Gamma$,$\Sigma$, $\Psi\rangle$, $\varnothing$) =  $\bot$
then $\nexists$ e. $\mid$ e $\mid$ $\leq$ k and $\Gamma$; $\Sigma$ $\vdash$ e : $\Psi$.

The proof is using Lemma <ref> and using the fact that CDCL (Algorithm 1, main-body) does
an exhaustive search over the ${S_k}^{\Psi}$, for a given $\Psi$ and k.

§.§ Implementation

An anonymized Implementation is available at :

§.§ Query Specifications

In this section we present a listing and a high-level description of the queries used in our evaluation:

§.§.§ Database Queries

Queries over the Newsletter Database
(*Unsubscribe a subscribed user to a newletter*)
D1 : (n  :  v : nl | true)-> (u :  v : user | true) ->
State \(h : heap).
\(D : [nlrecord]).
dsel (h, d) = D /\
nlmem (D , n , u) = true /\
subscribed (D, n, u) = true /\
confirmed (D, n, u) = false}
v : { v : unit | true}
{\(h: heap),(v : unit),(h': heap).
\(D : [nlrecord]), (D' : [nlrecord]).
(dsel (h', d) = D' /\
dsel (h, d) = D) =>
(nlmem (D', n, u) = true /\
subscribed (D', n, u) = false)
(*subscribe a user to a newsletter*)
D2 :  (n  : { v : nl | true})->
(u : { v : user | true}) ->
State {\(h : heap).
\(D : [nlrecord]).
dsel (h, d) = D /\
nlmem (D , n , u) = true /\
subscribed (D, n, u) = false /\
confirmed (D, n, u) = false}
v : { v : unit | true}
{\(h: heap),(v : unit),(h': heap).
\(D : [nlrecord]), (D' : [nlrecord]).
(dsel (h', d) = D' /\
dsel (h, d) = D) =>
(nlmem (D', n, u) = true /\
subscribed (D', n, u) = true /\
confirmed (D', n, u) = false)
(*remove a newletter, user pair from Database D*)
D3 : (n  : { v : nl | true})->
(u : { v : user | true}) ->
State {\(h : heap).
\(D : [nlrecord]).
dsel (h, d) = D /\
nlmem (D , n , u) = true /\
subscribed (D, n, u) = true /\
confirmed (D, n, u) = false}
v : { v : unit | true}
{\(h: heap),(v : unit),(h': heap).
\(D : [nlrecord]), (D' : [nlrecord]).
(dsel (h', d) = D' /\
dsel (h, d) = D)
=> (nlmem (D', n, u) = false)
(*read articles for a given user for a given newsletter *)
D4 :  (n  : { v : nl | true})->
(u : { v : user | true}) ->
State {\(h : heap).
\(D : [nlrecord]).
dsel (h, d) = D /\
nlmem (D , n , u) = true /\
subscribed (D, n, u) = false /\
confirmed (D, n, u) = false}
v : { v : [string] | true}
{\(h: heap),(v : [string]),(h': heap).
\(D : [nlrecord]), (D' : [nlrecord]).
(dsel (h', d) = D' /\
dsel (h, d) = D ) =>
(nlmem (D', n, u) = true /\
v = articles (D'))};
(*read the list of articles for a newletter and a user and then remove the pair from the database*)
D5 : (n  : { v : nl | true})->
(u : { v : user | true}) ->
State {\(h : heap).
\(D : [nlrecord]).
dsel (h, d) = D /\
nlmem (D , n , u) = true /\
subscribed (D, n, u) = true /\
confirmed (D, n, u) = true }
v : { v : [string] | true}
{\(h: heap),(v : [string]),(h': heap).
\(D : [nlrecord]), (D' : [nlrecord]).
(dsel (h', d) = D' /\
dsel (h, d) = D ) =>
(v = articles (D') /\
nlmem (D', n, u) = false)};

\end{lstlisting}
\paragraph{Queries over the Firewall Database}
\begin{lstlisting}[basicstyle=\small\tt,breaklines=true,language=ML]
(*remove a device d from the Device Table *)
D6 : (d : { v : int | true}) ->
(x : { v : int | not [v = d]}) ->
State {\(h: heap).
\(D : [int]).
didsel (h, dtab) = D /\
device (D, d) = true /\
device (D, x) = true }
v : {v : int | true}
{\(h: heap),(v : int),(h': heap).
\(D: [int]),(D' : [int]).
didsel (h', dtab) = D' =>
device (D', d) = false
(*add a device x and make a new connection with d*)
D7 : (d : { v : int | true}) ->
(x : { v : int | not [v = d]} ->
State {\(h: heap).
\(D : [int]), (CS : [srpair]).
didsel (h, dtab) = D /\
dcssel (h, cstab) = CS /\
device (D, d) = true /\
device (D, x) = false
v : {v : unit | true}
{\(h: heap),(v : unit),(h': heap).
\(D' : [int]),(CS' : [srpair]).
(didsel (h', dtab) = D' /\
dcssel (h', cstab) = CS' ) =>

device (D', x) = true /\
cansend (CS', d, x) = true)
(*make d non-central, remove device d, add device x and make x the central device *)
D8 : (d : { v : int | true}) ->
(x : { v : int | not [v=d]}) ->
State {\(h: heap).
\(D : [int]),(CS : [srpair]).
didsel (h, dtab) = D /\
device (D, d) = true /\
dcssel (h, cstab) = CS /\
device (D, x) = true /\
central (CS, d) = true /\
central (CS, x) = false}
v : {v : unit | true}
{\(h: heap),(v : unit),(h': heap).
\(D: [int]),(D' : [int]),(CS' :[srpair]).
(dcssel (h', cstab) = CS' /\
didsel (h', dtab) = D') =>
(device (D', d) = false /\
device (D', x) = true /\
central (CS', d) = false /\
central (CS', x) = true)};