
Hello:
I want to represent some relations in Dafny and state that they follow certain properties like transitivity, antisymmetry or totalness.
For example, suppose we want to declare a binary relation on a type T which is a total preorder relation. We may write the following predicate along with its three properties ( Reflexive is superfluous because
Total is harder, unless == does something strange, I think).
predicate Leq<T>(x : T, y : T)
// Reflexive
ensures x == y ==> Leq(x, y)
// Transitive
ensures forall z : T :: Leq(x, z) && Leq(z, y) ==> Leq(x, y)
// Total
ensures Leq(x, y)  Leq(y, x)
method Main()
{
var a : int, b : int, c : int;
assume Leq(a, b);
assume Leq(b, c);
// Transitivity
assert Leq(a, c);
// Reflexivity
assert Leq(a, a);
var x : int, y : int;
assume !Leq(x, y);
// Totalness
assert Leq(y, x);
}
This function can be used in any other function or method taking advantage of its properties, as in this example. But the function verification itself fails and Dafny complains about termination in the second and third postconditions.
A lemma might be used instead but it seems to be quite uncomfortable. I want to abstract from the particular relation definition. What is the better way to represent that in Dafny?
Thanks in advance.



I don't see immediately how you can do this. You need to prove that the predicate is defined. The terminiation error means that Dafny can't prove it is defined.
Here are some random thoughts:
To show termination you would somehow have to show that the predicate terminiates in a finite number of steps. The fact that T has no ordering makes it difficult. Could you provide a witness to the number of recursive steps required for
Leq ?
The lemma version would look like the following:
predicate Leq<T>(x : T, y : T)
lemma LeqTotalPreorder<T>(x : T, y : T)
// Reflexive
ensures x == y ==> Leq(x, y)
// Transitive
ensures forall z : T :: Leq(x, z) && Leq(z, y) ==> Leq(x, y)
// Total
ensures Leq(x, y)  Leq(y, x)
method Main()
{
var a : int, b : int, c : int;
assume Leq(a, b);
assume Leq(b, c);
// Transitivity
LeqTotalPreorder(a,c);
assert Leq(a, c);
// Reflexivity
LeqTotalPreorder(a,a);
assert Leq(a, a);
var x : int, y : int;
assume !Leq(x, y);
// Totalness
LeqTotalPreorder(x,y);
assert Leq(y, x);
}


Developer
Apr 19, 2016 at 4:12 PM

One option would be to write your predicate without any ensures initially, write a lemma ensuring its properties, and then write a wrapper around the original predicate. It can provide ensures about the original predicate without running into termination
errors, and it can call the lemma to make proving those properties easier.
Another option, which might be more what you're looking for, is to use Dafny's support for higherorder functions. For example, you could write something like this:
method Test(ghost R:(int,int)>bool)
requires forall x, y :: R.requires(x,y);
requires forall x, y :: x == y ==> R(x, y);
requires forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z);
requires forall x, y :: R(x, y)  R(y, x);
predicate Leq(x:int, y:int)
{
x <= y
}
method Main()
{
Test(Leq);
}
If you want to talk about lots of relations that have those properties, you could abstract the requires on Test into a predicate of its own.
Hope this helps.


Apr 23, 2016 at 8:55 PM
Edited Apr 23, 2016 at 8:56 PM

Thanks! The use of higherorder functions is what I was looking for and it seems to work ok.
For the sake of completeness, I will briefly write what I have tried following
parno's suggestions. The predicate " the argument is a total preorder relation" may be written like that:
predicate TotalPreorder(R : (T, T) > bool)
reads R.reads
{
(forall x, y :: R.requires(x, y))
&& (forall x, y, z :: R(x, y) && R(y, z) ==> R(x, z))
&& (forall x, y :: R(x, y)  R(y, x))
}
The wrapper method has also worked, but I find it less convenient.
predicate LeqDef(x : int, y : int)
{
x <= y
}
lemma LeqIsTotal(x : int, y : int)
ensures LeqDef(x, y)  LeqDef(y, x)
{
}
predicate Leq(x : int, y : int)
ensures LeqDef(x, y)  LeqDef(y, x)
{
LeqIsTotal(x, y); LeqDef(x, y)
}
And in response to lexicalscope, in the following example it is clear that the predicate ends in a finite number of steps but Dafny keeps complaining about termination errors:
predicate Leq(x : nat, y : nat)
ensures Leq(x, y)  Leq(y, x)
// decreases 0
{
true
}

