CODEWITHSUNDEEP
dafny
josephjnk
josephjnk

Reputation: 348

Can I allow preconditions on the argument to a higher-order function in Dafny?

Is there a way to say that a higher-order function permits preconditions on the function it takes as an argument?

Here's the concrete situation I'm trying to solve. I wrote this function for filtering items in a seq based on a predicate:

function method filterSeq<T>(s: seq<T>, fn: T -> bool): seq<T>
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: fn(filterSeq(s, fn)[i]) == true
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: filterSeq(s, fn)[i] in s
  ensures forall i | 0 <= i < |s| :: fn(s[i]) ==> s[i] in filterSeq(s, fn)
  {
    if |s| == 0 then [] else (
      if fn(s[0]) then [s[0]] + filterSeq(s[1..], fn) else filterSeq(s[1..], fn)
    )
  }

This covers the postconditions I care about, but doesn't say anything about the argument to fn. I want to say that for any property which holds for all T in s, this property is permitted as a precondition on fn.

The problem that lead me to this was an attempt to filter a sequence containing other sequences:

var sequences := [[1, 2, 3], [4, 5, 6], [7, 8, 9]];
assert forall i | 0 <= i < |sequences| :: |sequences[i]| == 3;

var result := filterSeq(sequences, sequence => sequence[0] == 4);

When I attempt this, I get an error on sequence[0], which says index out of range. Fair enough, I try to add a precondition to the lambda:

var sequences := [[1, 2, 3], [4, 5, 6], [7, 8, 9]];

assert forall i | 0 <= i < |sequences| :: |sequences[i]| == 3;

var result := filterSeq(sequences,
  sequence requires |sequence| == 3 => sequence[0] == 4);

Now I get the error value does not satisfy the subset constraints of 'seq<int> -> bool' (possible cause: it may be partial or have read effects) on the lambda argument. This also makes sense, I'm passing a partial function where I wrote the type signature for a non-partial one.

My question is: How do I change filterSeq to allow this? Can I somehow write it so that it will work with arbitrary preconditions, or will I have to write a separate filterSeqOfSequences method to cover this specific use-case?

Upvotes: 4

Views: 312

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Great question. The answer is yes. You need to use Dafny's notion of partial functions, which are written with a doubly-dashed arrow like T --> bool. If f has this type, then f.requires is its precondition. (In fact, you can think of the total function type T -> bool as a special case of T --> bool where f.requires is true for all values of type T.)

Here is one way to rewrite your higher-order function to accept a partial function as an argument:

function method filterSeq<T>(s: seq<T>, fn: T --> bool): seq<T>
  requires forall x | x in s :: fn.requires(x)        // ***
  ensures forall x | x in filterSeq(s, fn) :: x in s  // ***
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: fn(filterSeq(s, fn)[i]) == true
  ensures forall i | 0 <= i < |filterSeq(s, fn)| :: filterSeq(s, fn)[i] in s
  ensures forall i | 0 <= i < |s| :: fn(s[i]) ==> s[i] in filterSeq(s, fn)
{
  if |s| == 0
  then []
  else if fn(s[0]) 
  then [s[0]] + filterSeq(s[1..], fn) 
  else filterSeq(s[1..], fn)
}

method Test()
{
  var sequences := [[1, 2, 3], [4, 5, 6], [7, 8, 9]];

  assert forall i | 0 <= i < |sequences| :: |sequences[i]| == 3;

  var result := filterSeq(sequences,
    sequence requires |sequence| == 3 => sequence[0] == 4);
}

I just made two changes to your code, marked by ***.

First is the new precondition on filterSeq that you already mentioned in your question that requires that fn.requires holds on all elements of s. Second, we also need one new technical postcondition that guarantees the output of filterSeq is a subset of its input. This is needed to ensure the well formedness of the other postconditions, which try to call fn on elements of the output.

The Test method does not change at all. It just works with the new version of filterSeq.

Upvotes: 4

Related Questions