Кто может пояснить на примере. Есть программа:

using System.Diagnostics.Contracts;

namespace ConsoleApplication16
{
    class Program
    {
        public class Order
        {
            private decimal _orderPrice;

            [ContractInvariantMethod]
            private void objectInvariant()
            {
                Contract.Invariant(_orderPrice >= 0, "Цена не может быть меньше нуля.");
            }
        }

        static void Main(string[] args)
        {
            var o = new Order();
        }
    }
}

При запуске компиляции Warning: Warning 2 CodeContracts: ConsoleApplication16.Program+Order.#ctor()[0x6]: invariant unproven: _orderPrice >= 0 (Цена не может быть меньше нуля.) 1 1 ConsoleApplication16

Вроде _orderPrice приватная, внутри класса не вызывается вообще и всегда >= 0. Как нужно доказать компилятору, что она всегда >=0?

Здравствуйте, 0K, Вы писали:

0K>Вроде _orderPrice приватная, внутри класса не вызывается вообще и всегда >= 0. Как нужно доказать компилятору, что она всегда >=0?

Инициализировать ее?

Здравствуйте, 0K, Вы писали:

странно, если decimal поменять на double, то все нормально проходит
наверно надо копать в сторону decimal, что то с ним не то...

или можно сделать так
Contract.Invariant((double)_orderPrice >= 0, "Цена не может быть меньше нуля.");

Здравствуйте, 0K, Вы писали:

0K>Вроде _orderPrice приватная, внутри класса не вызывается вообще и всегда >= 0. Как нужно доказать компилятору, что она всегда >=0?

К сожалению, механизм контрактов (равно как и Pex) не понимает тип decimal. Для них он является неким непрозрачным типом с неизвестным поведением. Попробуй заменить на int или long.