Liquid Types vs. FloydHoare Logic
Several folks who are experts in the program verification literature have asked me some variant of the following question:
How are Liquid/Refinement types different from FloydHoare logics?
This question always reminds me of Yannis Smaragdakis' clever limerick:
No idea is too obvious or dreary,
If appropriately expressed in type theory,
It's a research advance,
That no one understands,
But they are all too impressed to be leery.
That is, the above question can be rephrased as: why bother with the hassle of encoding properties in types when good oldfashioned assertions, pre and postconditions would do? Is it just a marketing gimmick to make readers too impressed to be leery?
The Problem: Quantifiers¶
The main algorithmic problem with classical FloydHoare logic is that to do useful things, you need to use universally quantified logical formulas inside invariants, pre and postconditions.
Verification then proceeds by asking SMT solvers to check verification conditions (VCs) over these quantified formulas. While SMT solvers are marvelous technological artifacts, and I bow to no one in my admiration of them, in reality, they work best on formulas from a narrowly defined set of decidable theories.
In particular, they are notoriously (and justifiably!) fickle when quizzed on VCs with quantifiers. Briefly, this is because even if the solver "knows" the universally quantified fact:
forall x. P(x)
the solver doesn't know which particular terms e1
, e2
or e3
to instantiate the fact at. That is, the solver doesn't know
which P(e1)
or P(e2)
or P(e3)
it should work with to prove
some given goal. At best, it can make some educated guesses, or
use hints from the user, but these heuristics can turn out to be
quite brittle as the underlying logics
are undecidable in general. To make verification predictable,
we really want to ensure that the VCs remain decidable, and
to do so, we must steer clear of the precipice of quantification.
The Solution: Types¶
The great thing about types, as any devotee will tell you, is that the compose. Regrettably, that statement is only comprehensible to believers. I prefer to think of it differently: types decompose. To be precise:
Types decompose quantified assertions into quantifierfree refinements.
Let me make my point with some examples that show what verification looks like when using Refinement Types (as implemented in LiquidHaskell) vs FloydHoare style contracts (as implemented in Dafny).
The goal of this exercise is to illustrate how types help with verification, not to compare the tools LH and Dafny. In particular, Dafny could profit from refinement types, and LH could benefit from the many clever ideas embodied within Dafny.
Example 1: Properties of Data¶
Consider the following standard definition of a List
datatype
in Dafny (left) and LH (right).
(You can see the full definitions for Dafny and LiquidHaskell.)
Accessing a list¶
The two descriptions are more or less the same except for some
minor issues of concrete syntax. However, next consider the
respective implementations of a function to access the ith
element of a List
. We also pass in a def
ault value returned
when the index i
is invalid.
It is (usually) silly to access lists in this fashion.
I use this example merely to illustrate the common case
of defining a container structure (here, List
) and
then accessing its contents (here, ith
).
As such, we'd like to specify that the value returned
by the ith
element is indeed in the container or is
the def
ault.
FloydHoare Logic
With classical FloydHoare logic, as shown in the Dafny listing
on the left, we must spell out the specification quite explicitly.
The programmer must write an elements
function that describes
the set of values in the container, and then the postcondition
of ith
states that the res
is either in that set or the default.
While this specification seems simple enough, we are already on
dicey terrain: how are we to encode the semantics of the
userdefined function elements
to the SMT solver?
In the classical FloydHoare approach, we must use a
quantified invariant of the form:
elements(Nil) = empty
&& forall h t :: elements(Cons(h, t)) = {h} + elements(t)
Thanks to the ingenuity of Greg Nelson who invented the notion
of triggers and of Rustan Leino and many others, who devised
ingenious heuristics for using them, Dafny handles the quantifier
calmly to verify the above specification for ith
.
However, we are not always so fortunate: it frightfully easy
to run into quantifierrelated problems with userdefined
functions, as we will see in due course.
Liquid/Refinement Types
In contrast, the liquid/refinement version is quite spare: there is no extra specification beyond the code. Surely there must be some mistake? Look again: the type signature says everything we need:
If you call
ith
with a list ofa
values and a defaulta
value then you get ana
value".
That is parametricity removes the overhead of using an
explicit elements
function.
Building a list¶
Next, lets extend our example to illustrate the common
situation where we want some invariant to be true for
all the values in a container. To this end, let us
write a function mkList
that builds a container
with values k+1
,...,k+n
and then test that when
k
is nonnegative, any arbitrarily chosen value from
the container is indeed strictly positive.
The code in Dafny and LH is more or less the same, except for one crucial difference.
FloydHoare Logic
Recall that the specification for ith(pos, i, 1)
states
that the returned value is some element of the container
(or 1
). Thus, to verify the assert
in testPosN
using
classical FloydHoare logic, we need a way to specify that
every element in pos
is indeed strictly positive.
With classical program logics, the only way to do so is to
use a universally quantified postcondition, highlighted
in blue:
"for all v
if v
is in the elements of the res
ult, then v
is greater than k
"
Liquid/Refinement Types
Regardless of my personal feelings about quantifiers,
we can agree that the version on the right is simpler
as types make it unnecessary to mention elements
or
forall
. Instead, LH infers
mkList :: Int > k:Int > List {v:Int  k < v}
That is, that the output type of mkList
is a
list of values v
that are all greater than k
.
The scary forall has been replaced by the friendly
type constructor List
. In other words, types
allow us to decompose the monolithic universally
quantified invariant into:
 a quantifierfree refinement
k < v
, and  a type constructor that implicitly "quantifies" over the container's elements.
Lesson: Decomposition Enables Inference¶
Am I cheating? After all, what prevents Dafny from inferring the same postcondition as LH?
Once again, quantifiers are the villain.
There have been many decades worth of papers on the topic of inferring quantified invariants, but save some nicely circumscribed usecases these methods turn out to be rather difficult to get working efficiently and predictably enough to be practical. In contrast, once the quantifiers are decomposed away, even an extremely basic approach called Monomial Predicate Abstraction, or more snappily, Houdini, suffices to infer the above liquid type.
Example 2: Properties of Structures¶
Recall that when discussing the userdefined elements
function above,
I had issued some dark warnings about quantifierrelated problems that
arise from userdefined functions. Allow me to explain with another
simple example, that continues with the List
datatype defined above.
(You can see the full definitions for Dafny and LiquidHaskell.)
Specifying a size
Function¶
Lets write the usual recursive function that computes the size
of a list. The definitions are mostly identical, except for the green
measure
highlight that we will discuss below.
FloydHoare Logic
SMT solvers are restricted to a set of ground theories and hence,
do not "natively" understand userdefined functions. Instead, the
verifer must teach the SMT solver how to reason about formulas (VCs)
containing uses of userdefined functions like size
.
In the classical FloydHoare approach, this is done by converting
the definition of size
into a universally quantified axiom like:
size Nil == 0 && forall h, t :: size (Cons h t) = 1 + size t
A quantifier! By the pricking of my thumbs, something wicked this way comes...
Liquid/Refinement Types
With a more typecentric view, we can think of the recursive
function size
as a way to decorate or refine the types of
the data constructors. So, when you write the definition in
the green box above, specifically when you add the measure
annotation, the function is converted to strengthened
versions for the types of the constructors Nil
and Cons
,
so its as if we had defined the list type as two constructor
functions
data List a where
Cons :: h:a > t:List a > {v:List a  size v == 1 + size t}
Nil :: {v:List a  size v == 0}
That is, the bodies of the measures get translated to refinements
on the output types of the corresponding constructors. After this,
the SMT solver "knows nothing" about the semantics of size
, except
that it is a function. In logicspeak, size
is uninterpreted
in the refinement, and there are no quantified axioms. That is, we
choose to keep SMT solver blissfully ignorant about the semantics
of size
. How could this possibly be a good thing?
Verifying the size
of a List¶
Next, lets see what happens when we write a simple test that builds
a small list with two elements and assert
s that the lists size
is indeed 2
:
FloydHoare Logic
To get Dafny to verifier to sign off on the assert (size(pos) == 2)
we have to add a mysterious extra assertion that checks the size of
the intermediate value Cons (1, Nil)
. (Without it, verification fails.)
Huh? Pesky quantifiers.
The SMT solver doesn't know where to instantiate the size
axom.
In this carefully chosen, but nevertheless simple situation, Dafny's
instantiation heuristics come up short. I had to help them along by
guessing this intermediate assertion, which effectively "adds" the
fact that the size of the intermediate list is 1, thereby letting
the SMT solver prove the second assertion.
Liquid/Refinement Types
In contrast, with types, the solver is able to verify the code without
batting an eyelid. But how could it possibly do so even though we kept
it ignorant of the semantics of size
?
Because types decompose reasoning. In particular, here, the measure
and constructor trick lets us factor reasoning about size
into the type system.
In particular, LH internally views the code for test
in ANormal Form
which is a fancy way of saying, by introducing temporary variables
for all subexpressions:
test x1 =
let tmp0 = Nil
tmp1 = Cons x1 tmp0
pos = Cons 0 tmp1
in
assert (size pos == 2)
And now, just by the rules of type checking, and applying the types of the constructors, it deduces that:
tmp0 :: {size tmp0 == 0}
tmp1 :: {size tmp1 == 1 + size tmp0}
pos :: {size pos == 1 + size tmp1}
which lets the SMT solver prove that size pos == 2
without
requiring any axiomatic description of size
. This simple
measure
method goes a very long way in specifying and
verifying lots of properties.
Lesson: Decomposition Enables TypeDirected Instantiation¶
I'd like to emphasize again that this trick was enabled by the typecentric view: encode the function semantics in data constructors, and let the type checking (or VC generation) do the instantiation.
It could easily by incorporated inside and work together with axioms in FloydHoare based systems like Dafny. Of course, this approach is limited to a restricted class of functions  roughly, casesplits over a single data type's constructors  but we can generalize the method quite a bit using the idea of logical evaluation.
Summary¶
To sum up, we saw two examples where taking a typecentric view made verification more ergonomic, essentially by factoring reasoning about quantifiers into the type system.

In the first case, when reasoning about data in containers, the polymorphic type constructor
List
provided an natural way to reason about the fact that all elements in a container satisfied some property. 
In the second case, when reasoning about the structure of the container via a recursive function, the types of the data constructors allowed us to factor the instantiation of properties of
size
at places where the list was constructed (and dually, not shown, destructed) without burdening the SMT solver with any axioms and the pressure of figuring out where to instantiate them.
To conclude I'd like to reiterate that the point is not that types and program logics are at odds with each other. Instead, the lesson is that while classical FloydHoare logic associates invariants with program positions, Liquid/Refinement types are a generalization that additionally let you associate invariants with type positions, which lets us exploit
 types as a program logic, and
 syntaxdirected typing rules as a decision procedure,
that, in many common situations, simplify verification by
decomposing proof obligations (VCs) into simple, quantifierfree,
SMTfriendly formulas. As you might imagine, the benefits
are magnified when working with higherorder functions,
e.g. map
ing or fold
ing over containers...
Acknowledgments¶
Huge thanks to Rustan Leino, Nadia Polikarpova, Daniel Ricketts, Hillel Wayne, and Zizz Vonnegut for patiently answering my many questions about Dafny!