Jul 14, 2015 at 2:06 PM
Edited Jul 14, 2015 at 6:15 PM

I've seen a few references to Dafny supporting higherorder functions. What is the syntax for using and reasoning about higherorder functions in Dafny? Also, which versions of Dafny support it?
For instance, consider the following definition of a Haskell function that creates a sorting function based on an ordering function (which uses
Bool rather than Ordering simply to make the example more brief). Can I specify a similar function in Dafny and if yes, how would I do it?
 Using the following predicates for all comparator of type (a > a > Bool)
 and xs of type [a]:
 Sorted(comparator, xs) <==> forall i:int, j:int :: 0 <= i <= j < (length xs)
 ==> (comparator xs!!i xs!!j)
 Transitive(comparator) <==> forall x:a, y:a, z:a :: (comparator x y)
 && (comparator y z) ==> (comparator x z)
 Reflexive(comparator) <==> (...)
 Antisymmetric(comparator) <==> (...)
createSortingFunction :: (a > a > Bool) > ([a] > [a])
 ensures forall comparator:(a > a > Bool) :: Transitive(comparator)
 && Reflexive(comparator) && Antisymmetric(comparator)
 ==> forall xs:[a] :: Sorted(comparator,
 (createSortingFunction comparator) xs)
createSortingFunction comparator
= (...)
Cheers,
Benjamin EgelundMuller (Imperial College student working on a Dafny project).
(EDIT: Improved formatting)


Coordinator
Jul 28, 2015 at 12:20 AM

Hi Benjamin,
I've tried to answer your question by using the example you mention. Please ask as you'll have further questions. Also, the Test/hofs folder in the Dafny source distribution contains a number of examples of firstclass functions.
The code below is available on rise4fun as follows:
http://rise4fun.com/Dafny/OG5. However, note that there has been a recent change in Dafny that improves how reads clauses for higherorder functions are checked. This change is not yet reflected on rise4fun, so the rise4fun version needs some extra lines
of specifications (as I have indicated in the code).
Rustan
datatype List<A> = Nil  Cons(head: A, tail: List)
function Length(xs: List): nat
{
match xs
case Nil => 0
case Cons(_, tail) => 1 + Length(tail)
}
function Get<A>(xs: List, i: nat): A
requires i < Length(xs)
{
if i == 0 then xs.head else Get(xs.tail, i1)
}
// As you'd expect from Haskell, a firstclass function in Dafny has a type.
// In the following, I chose to write the type of the comparator as (A, A) > bool instead
// of A > A > bool.
// Note, btw, that A > B (equivalently, (A) > B, since parentheses are allowed around
// types) is a function of one argument and (A, B) > C is a function of two
// arguments. Note that, in the case of the latter, the parentheses give the grouping of
// the list of arguments. If you want to write a function that takes a pair, you write
// ((A, B)) > C, where the outer parentheses indicate that "here comes a commaseparated
// list of argument types" and the inner parenteses are Dafny's usual tupleforming type.
// As for functions and methods, Dafny allows a firstclass function to have a precondition.
// This precondition is not reflected in the type, but you can write specifications about
// it. Analogously, you can declare a variable to be of type integer, but you write specifications
// about what specific values the variable may have at certain times. For a function F: A > B,
// F.requires is a function A > bool that says which values fit satisfy the precondition of F.
// For example, for a of type A, expression F.requires(a) is a boolean that says whether or not
// F can be invoked on a.
// Furthermore, firstorder functions in Dafny can read the heap. These read effects are
// specified using reads clauses, and F.reads is an expression of type A > set<object> that
// tells you what the reads frame of F is. In most mathematical examples and in examples from
// functional programming, functions don't read the heap, so you may want to specify that
// the reads frame is empty.
// For the sorting example, we'll choose to say that the comparator is a total function (that is,
// one whose precondition is always true) without read effects:
predicate IsTotal<A>(comparator: (A, A) > bool)
reads comparator.reads
{
forall a,b :: comparator.reads(a,b) == {} && comparator.requires(a,b)
}
// (In the near future, I hope to support types and syntactic shorthands that more easily allow
// you to express the property I defined in the predicate above.)
predicate Sorted<A>(comparator: (A, A) > bool, xs: List)
requires IsTotal(comparator)
//reads comparator.reads
{
forall i,j :: 0 <= i < j < Length(xs) ==> comparator(Get(xs, i), Get(xs, j))
}
predicate Transitive<A>(R: (A, A) > bool)
requires IsTotal(R)
{
forall a,b,c :: R(a,b) && R(b,c) ==> R(a,c)
}
predicate Reflexive<A>(R: (A, A) > bool)
requires IsTotal(R)
{
forall a :: R(a,a)
}
predicate Antisymmetric<A>(R: (A, A) > bool)
requires IsTotal(R)
{
forall a,b :: R(a,b) && R(b,a) ==> a == b
}
// Note: A relation that is transitive, reflexive, and antisymmetric is called a _partial order_.
// You don't actually need antisymmetry for sorting, but you do what the order to be _total_:
predicate TotallyOrdered<A>(R: (A, A) > bool)
requires IsTotal(R)
{
forall x,y :: R(x,y)  R(y,x)
}
// The TotallyOrdered property implies reflexivity, as I prove here:
lemma TotalOrdersAreReflexive<A>(R: (A, A) > bool)
requires IsTotal(R) && TotallyOrdered(R)
ensures Reflexive(R)
{
}
function createSortingFunction<A>(comparator: (A, A) > bool): List<A> > List<A>
// I recommend adding the following precondition to the function, which lets you more
// quickly detect any attempted call to this function.
requires IsTotal(comparator)
requires Transitive(comparator) && TotallyOrdered(comparator)
ensures forall xs :: createSortingFunction(comparator).reads(xs) == {} && createSortingFunction(comparator).requires(xs)
// ...
// You could write the desired property of createSortingFunction as a postcondition. However,
// I think it will probably be easier to prove this property as a lemma.
lemma CreateSortingFunction_Property<A>(comparator: (A, A) > bool)
requires IsTotal(comparator)
requires Transitive(comparator) && TotallyOrdered(comparator)
ensures forall xs :: Sorted(comparator, createSortingFunction(comparator)(xs))
// ...

