在對像不變的程式碼中，我能有多自由？

我試圖在程式碼合同中展示不變數，我想我會舉一個字元串排序列表的例子。它在內部維護一個數組，有用於添加等的備用空間 - 基本上就像List<T>. 當它需要添加一個項目時，它將它插入到數組中，等等。我想我有三個不變數：

• 計數必須是合理的：非負數並且最多與緩衝區大小一樣大
• 緩衝區未使用部分中的所有內容都應為空
• 緩衝區已用部分中的每個項目都應至少與之前的項目一樣“大”

現在，我嘗試以這種方式實現它：

[ContractInvariantMethod]
private void ObjectInvariant()
{
   Contract.Invariant(count >= 0 && count <= buffer.Length);
   for (int i = count; i < buffer.Length; i++)
   {
       Contract.Invariant(buffer[i] == null);
   }
   for (int i = 1; i < count; i++)
   {
       Contract.Invariant(string.Compare(buffer[i], buffer[i - 1]) >= 0);
   }
}

不幸ccrewrite的是，正在搞亂循環。

使用者文件說該方法應該只是對Contract.Invariant. 我真的必須像這樣重寫程式碼嗎？

Contract.Invariant(count >= 0 && count <= buffer.Length);
Contract.Invariant(Contract.ForAll
   (count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll
   (1, count, i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

這有點難看，儘管它確實有效。（這比我之前的嘗試要好得多，請注意。）

我的期望不合理嗎？我的不變數不合理嗎？

（也在程式碼合同論壇中作為問題提出。我將自己在這裡添加任何相關答案。）

從（初步）MSDN 頁面看來，Contract.ForAll 成員可以幫助您處理 2 個範圍合同。但是，文件對它的功能並不是很明確。

//untested
Contract.Invariant(Contract.ForAll(count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll(1, count, 
   i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

引用自：https://stackoverflow.com/questions/1209185