Functional programs typically interact with
effectful libraries that hide state behind typed
abstractions. One particularly important class
of applications are data structure
implementations that rely on such libraries to
provide a level of efficiency and scalability
that may be otherwise difficult to
achieve. However, because the specifications of
the methods provided by these libraries are
necessarily general and rarely specialized to
the needs of any specific client, any required
application-level invariants must often be
expressed in terms of additional constraints on
the (often) opaque state maintained by the
library.
In this paper, we consider the specification and
verification of such representation invariants
using symbolic finite automata (SFA). We show
that SFAs can be used to succinctly and
precisely capture fine-grained temporal and
data-dependent histories of interactions between
functional clients and effectful libraries. To
facilitate modular and compositional reasoning,
we integrate SFAs into a refinement type system
to qualify effectful computations resulting from
such interactions. The particular instantiation
we consider, Hoare Automata Types (HATs), allows
us to both specify and automatically type-check
the representation invariants of a datatype,
even when its implementation depends on
effectful library methods that operate over
hidden state.
We also develop a new bidirectional type
checking algorithm that implements an efficient
subtyping inclusion check over HATs, enabling
their translation into a form amenable for
SMT-based automated verification. We present
extensive experimental results on an
implementation of this algorithm that
demonstrates the feasibility of type-checking
complex and sophisticated HAT-specified OCaml
data structure implementations layered on top of
effectful library APIs.
