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)))));