Contracts With Multiple Arguments

Question

I started coding with contracts in c#. I want to express the following property in c#

ISet<Tuple<A,B>> set;
Contract.Requires(!Contract.Exists(set, (e1,e2) => (((e1 != null) && (e2 != null)) &&    (e1.Item1 == e2.Item1) && (e1.Item2 != e2.Item2))));

i.e. if the first elements of two tuples are the same the second one should be the same aswell.

The problem here is that (e1,e2) => ... is not a valid expression because of the two arguments. Does anybody now how to express this contract with the both e1 and e2? Or how to rewrite it?

Answer 1

Thanks for the clarification with the template. What I wanted to say was the following:

\forall s,t in ISet< Tuple< A,B>>: (s.a==t.a) -> (s.b==t.b)

I guess it was somehow unclear. I finally solved it the following way (previously not knowing that it is possible to nest Contract.Exist and Contract.ForAll and after some logic reformulating)

ISet<Tuple<A,B> set;
Contract.Invariant(Contract.ForAll(set, s => s != null && Contract.ForAll(set, t => t != null && ((s.Item1 != t.Item1)||(s.Item2 == t.Item2)))));

Answer 2

Template argument of Contract.Exist() is collection element so in your case Tuple<A, B>. You can't disjoint them (A and B from Tuple<A, B> because for ISet<T> template T is Tuple<A, B>).

Rewrite it as (if I did understand you require tuple's elements aren't equal and they're not null, in case just change it):

Contract.Requires(!Contract.Exists(set,
    x => x.Item1 == null || x.Item2 == null || x.Item1 == x.Item2));