public class Order
{
    List<OrderItem> orderedItems = new List<OrderItem>();
    decimal orderPrice = 0;
    public void MakeNewOrder(OrderItem orderItem)
    {
      // precondition
      Contract.Requires<ArgumentNullException>(orderItem != null);
      Contract.Requires(Contract.ForAll(orderedItems, p => p != orderItem));
      // postcondition
      Contract.Ensures(Contract.Exists(orderedItems, p => p == orderItem));
      Contract.Ensures(orderPrice > Contract.OldValue(orderPrice));
      orderedItems.Add(orderItem);
      orderPrice += orderItem.Price;
    }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
      Contract.Invariant(orderPrice > 0);
    }    
}