  A representation invariant is a property that holds of all values of abstract
type produced by a module. Representation invariants play important roles in
software engineering and program verification. In this paper, we develop a
counterexample-driven algorithm for inferring a representation invariant that
is sufficient to imply a desired specification for a module. The key novelty is
a type-directed notion of visible inductiveness, which ensures that the
algorithm makes progress toward its goal as it alternates between weakening and
strengthening candidate invariants. The algorithm is parameterized by an
example-based synthesis engine and a verifier, and we prove that it is sound
and complete for first-order modules over finite types, assuming that the
synthesizer and verifier are as well. We implement these ideas in a tool called
Hanoi, which synthesizes representation invariants for recursive data types.
Hanoi not only handles invariants for first-order code, but higher-order code
as well. In its back end, Hanoi uses an enumerative synthesizer called Myth and
an enumerative testing tool as a verifier. Because Hanoi uses testing for
verification, it is not sound, though our empirical evaluation shows that it is
successful on the benchmarks we investigated.
