Если я напишу
[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
является перенаправлением постусловия, даже если я вызову его вызов как первую строку моего метода, он будет проверен как последний, непосредственно перед выходом из функции?