Function type attributes

Apr 30, 2016 at 12:41 PM
Hello.

I don't know why the following code produces an error. Dafny cannot prove that Property holds for the func attribute at the end of the constructor, whose body is a mere assignment to it from a parameter which already has that property.

If reads R.reads is removed from Property's definition, Dafny verifies it without trouble.
class Example<T>
{
    // A binary predicate variable
    var func : (T, T) -> bool;

    predicate {:opaque} Property(R : (T, T) -> bool)
        reads R.reads

    constructor(g : (T, T) -> bool)
        modifies this

        requires Property(g)
        ensures Valid()
    {
        func := g;
    }

    predicate Valid()
        reads this, func.reads
    {
        Property(func)
    }
}
The following program gets verified without any problem and it is essentially the same.
predicate {:opaque} Property<T>(f : (T, T) -> bool)
    reads f.reads

method Example<T>()
{
    var func1 : (T, T) -> bool;

    assume Property(func1);

    var func2 := func1;

    assert Property(func2);
}
May 13, 2016 at 10:51 AM
My guess is that because the Property has the same read set as g then when you write to the field func Dafny no longer knows that Property still holds.

In the second program we know that the function in func1 does not read the variable func2

So this does verify
class Example<T>
{
    // A binary predicate variable
    var func : (T, T) -> bool;

    predicate {:opaque} Property(R : (T, T) -> bool)
        reads R.reads

    constructor(g : (T, T) -> bool)
        modifies this
        requires forall t1,t2:T :: !(this in g.reads(t1,t2))
        requires Property(g)
        ensures Valid()
    {
        assert Property(g);
        func := g;
        assert Property(g);
    }
    

    predicate Valid()
        reads this, func.reads
    {
        Property(func)
    }
}
May 15, 2016 at 5:57 PM
Hello and thanks.

It works but when we try to add new methods to the class using the predicate attribute, we come back to obtain similar errors on those. The reason behind is most probably the same (that the predicate may depend on this, which has changed).

So I tried to add the new precondition's formula to the class invariant predicate, and then the constructor stops working. I have written the explicit problematic assert for clarity.
class Example<T>
{
    // A binary predicate variable
    var func : (T, T) -> bool;

    predicate {:opaque} Property(R : (T, T) -> bool)
        reads R.reads

    constructor(g : (T, T) -> bool)
        modifies this
        requires forall t1,t2:T :: !(this in g.reads(t1,t2))
        requires Property(g)
        ensures Valid()
    {
        func := g;

        assert forall t1,t2:T :: this !in func.reads(t1, t2);
    }


    predicate Valid()
        reads this, func.reads
    {
        Property(func)
        &&
        (forall t1,t2:T :: this !in func.reads(t1, t2))
    }
}
I find that mixing higher-order functions and generics in Dafny is a headache. Ideally, the function should depend in its arguments, but I guess it is impossible to declare such a thing because T could be a value or reference type and we cannot distinguish it (anyway it will be ugly). Even if that were possible, the argument themselves could have in turn references we may want to include in the read set... but this should not be included and...
May 16, 2016 at 9:17 AM
I think this is a problem with triggering the forall quantifer in the postcondition.

If you find yourself repeating a formula that contains a quantifer it is often productive to extract it into its own predicate. This avoids the need for Dafny to recongnise that it should instanciate both quantifiers the same way (since now there is now - syntatically - only one quantifer).
class Example<T>
{
    // A binary predicate variable
    var func : (T, T) -> bool;

    predicate {:opaque} Property(R : (T, T) -> bool)
        reads R.reads

    constructor(g : (T, T) -> bool)
        modifies this
        requires f(g)
        requires Property(g)
        ensures Valid()
    {
        func := g;

        //assert f(func);
    }

    predicate f(g : (T, T) -> bool)
       reads g.reads
    {
      forall t1,t2:T :: this !in g.reads(t1, t2)
    }

    predicate Valid()
        reads this, func.reads
    {
        Property(func)
        &&
        f(func)
    }
}
May 16, 2016 at 12:56 PM
It works. Thanks for your quick reply. Defining new predicates seems to be very helpful in many situations.

However, when we try to extend this code other problems arise. I have added an array to the example and a method which modifies it. The array is another reference the predicate variable may depend on, so whenever the array is changed the predicate is invalidated (a new method AMethod has been included as an example). Thus we should express that the predicate does not depend on anArray but in order to access this field from GoodPredicate we ought to include this in its read set. And then GoodPredicate is invalidated every time the object changes.

As I said in the previous message, I think that the idea behind this example, that of programming and specifying a generic data structure (a sorted list with an arbitrary comparator given as a parameter, for instance), will not prosper in current Dafny.
predicate {:opaque} Property<T>(R : (T, T) -> bool)
    reads R.reads

class Example<T>
{
    // A binary predicate variable
    var func : (T, T) -> bool;

    var anArray : array<T>;

    predicate GoodPredicate(g : (T, T) -> bool)
        reads g.reads
        reads this
    {
        forall t1,t2:T :: this !in g.reads(t1, t2) &&
            anArray !in g.reads(t1, t2)
    }

    constructor(g : (T, T) -> bool)
        modifies this

        requires GoodPredicate(g)
        requires Property(g)

        ensures Valid()
    {
        func := g;
        anArray := new T[2];
    }

    method AMethod()
        modifies this, anArray

        requires Valid()
        ensures Valid()
    {
        anArray[0] := anArray[1];
    }

    predicate Valid()
        reads this, func.reads
    {
        Property(func)
        &&
        GoodPredicate(func)
        &&
        anArray != null
        &&
        anArray.Length > 1
    }
}
May 18, 2016 at 12:46 PM
I do not know how to resolve this. Perhaps looking at the reads clauses of some example comparators may offer some insight?

An alternative approach could be to use a trait and pass the comparator as an object rather than a function. However, I think that generic traits are not currently supported so this might not be possible in your case.
trait Comparator
{
  method Compare<T>(o1: T, o2: T) returns (result : int)
}