c# - 具有多个参数的合同

Question

我开始使用 c# 中的合同进行编码。我想在 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))));

即如果两个元组的第一个元素相同，则第二个元素也应该相同。

这里的问题是 (e1,e2) => ... 由于有两个参数，它不是一个有效的表达式。有人现在如何用 e1 和 e2 表达这个合同吗？或者如何重写？

Answer 1

感谢您对模板的澄清。我想说的是：

\forall s,t in ISet< Tuple< A,B>>: (sa==ta) -> (sb==tb)

我想这有点不清楚。我终于通过以下方式解决了它（以前不知道可以嵌套 Contract.Exist 和 Contract.ForAll 并且经过一些逻辑重新制定）

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

的模板参数Contract.Exist()是集合元素，所以在你的情况下Tuple<A, B>。您不能将它们分开（A并且BfromTuple<A, B>因为 for ISet<T>template Tis Tuple<A, B>）。

将其重写为（如果我确实理解您需要元组的元素不相等并且它们不是null，以防万一更改它）：

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