Я считаю, что следующее должно сделать трюк:
Contract.Requires(
Contract.ForAll(
coll,
obj => (coll.Where(x=>x.PropA = obj.PropA).Count==1)
)
);
Теория состоит в том, что фильтры фильтруют только те элементы, значение PropA которых совпадает с объектом, на который мы смотрим. Должен быть только один из них (сам).
Вы можете повторить то же самое для B.
И теоретически объединять лямбда-выражения ForAll тривиально, но я не уверен, что вы захотите. Конечно, было бы неплохо знать, какое условие терпит неудачу, если кто-то делает это, а не смешивать их все вместе и знать, что что-то не удалось, но на самом деле не то, что ...
Если вы можете дать немного свободы в формате, который вы можете попробовать:
Contract.Requires(
Contract.ForAll(
coll.GroupBy(x=>x.PropA),
group => group.Count==1)
)
);
Это аналогичный принцип, но я думаю, что будет делать подсчет более эффективно, поскольку группировка по и подсчет будет более эффективной (я думаю - я не проверял и не знаком с внутренней работой методов linq).
Другой метод:
HashSet<object> propAValues = new HashSet<object>();
Contract.Requires(
!coll.Any(x=>!hashset.Add(x.PropA))
);
При этом используется хэш-набор и тот факт, что Add возвращает false, если элемент уже существует. В этом случае в тот момент, когда Add генерирует ложное значение (и, следовательно, лямбда-выражение равно true), Any возвращает true, которое, поскольку оно отменено, не пройдёт тест.
Является ли этот метод разумным или нет, вероятно, зависит от того, насколько велики ваши объекты (и, следовательно, от возможных последствий для памяти удвоения вашего набора объектов. Однако для завершения потребуется меньше всего итераций по сравнению с другими методами здесь (поскольку другой Методы должны просматривать каждый объект в коллекции, возможно, несколько раз, тогда как последний может потенциально остановиться после просмотра двух записей).