Higher-order functions in Dafny

Jul 14, 2015 at 2:06 PM
Edited Jul 14, 2015 at 6:15 PM
I've seen a few references to Dafny supporting higher-order functions. What is the syntax for using and reasoning about higher-order 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 Egelund-Muller (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 first-class 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 higher-order 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, i-1)
}

// As you'd expect from Haskell, a first-class 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 comma-separated
// list of argument types" and the inner parenteses are Dafny's usual tuple-forming type.

// As for functions and methods, Dafny allows a first-class 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, first-order 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))
// ...