Предварительные условия и постусловия в CodeContracts - PullRequest
1 голос
/ 05 августа 2011

Если я напишу

 [Pure]
 static string s10 {get;set;}

 static void Main(string[] args)
 {
     Contract.Ensures(s10.Length <= 10); //Contract fails
     s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
 }

Поскольку у меня нет Premium версии VS, поэтому нет статической проверки, после запуска программы VS сообщает мне о проблеме: Postcondition failed: s10.Length <= 10, хорошо.

если я напишу, вместо

 [Pure]
 static string s10 {get;set;}

 static void Main(string[] args)
 {
    Contract.Requires(s10.Length <= 10); //NullReferenceException
    s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
 }

VS сообщает мне исключение нулевой ссылки.

Действительно ли это означает, что, поскольку Ensures является перенаправлением постусловия, даже если я вызову его вызов как первую строку моего метода, он будет проверен как последний, непосредственно перед выходом из функции?

1 Ответ

3 голосов
/ 05 августа 2011

Да - переписчик Code Contracts перемещает код в нужное место, а также несколько других вещей.Стоит посмотреть на результат в Reflector, чтобы увидеть, что происходит.

I сильно советуем вам внимательно прочитать руководство пользователя, которое поставляется с Code Contracts.Из того, что я помню, это отличная документация.

...