Проблемы с Contract.Requires () и инвариантом цикла - PullRequest
Новая
       42

Проблемы с Contract.Requires () и инвариантом цикла

0 голосов
/ 08 мая 2019

Я следую учебному пособию по кодексам (https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#usage-guidelines), и мне кажется, что я не могу заставить работать самую простую вещь. Учитывая определение метода 

public int Add(int x, int y)
{
   Contract.Requires(x > 0);
   Contract.Requires(y > 0);

   return x+y;
}

, когда я вызываю o.Add(0,0) методне проходит проверку предварительного условия. Когда я нахожусь в режиме отладки, пропускаются операторы Contract.Requires(). Где я делаю неправильно?

Второй вопрос: можно ли использовать Contract.Invariant() для проверки инварианта цикла?к определению инварианта объекта Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client., который, кажется, немного отличается от инварианта цикла, так как в каждой итерации цикла инвариант цикла может не обязательно быть видимым для клиента, поэтому он может нарушать свойство, но не проверяться. Является ли это понимание правильным??

1 Ответ

0 голосов
/ 14 мая 2019

В ответ на ваш первый вопрос загрузите и запустите MSI-файл Code Contracts с здесь . MSI-файл включает в себя статическую проверку и бинарный перезаписчик (для проверки во время выполнения), который модифицирует программу, вводя контракты, заставляя их проверяться как часть выполнения программы. Без переписчика контракты проверяться не будут. Обратите внимание, что программа перезаписи работает только с Visual Studio 2013 и 2015.

В ответ на ваш второй вопрос вы не можете использовать Contract.Invariant() для проверки инварианта цикла. Я бы предложил использовать Contract.Assume() в цикле.

...