Кодовите договори предупреждават за недоказани гаранции, когато са включени брави

Опитвам се да разбера как .NET Code Contracts взаимодействат с ключовата дума lock, използвайки следния пример:

public class TestClass
{
  private object o1 = new object();
  private object o2 = new object();

  private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      this.o1 = new object();
    }
  }
}

Когато стартирам инструмента за статичен анализ на Code Contract, той отпечатва предупреждение: Ensures unproven: this.o1 != null

Ако направя някое от:

  • променете o2 в lock на o1,
  • променете o1 вътре в блока lock на o2,
  • добавяне на втори ред вътре в блока lock присвояване на new object на o2
  • променете lock (this.o2) на if (this.o2 != null),
  • премахнете изцяло оператора lock.

предупреждението изчезва.

Въпреки това, промяната на реда вътре в блока lock на var temp = new object(); (като по този начин премахва всички препратки към o1 от метода) все още причинява предупреждението:

private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      var temp = new object();
    }
  }

Така че има два въпроса:

  1. Защо се появява това предупреждение?
  2. Какво може да се направи, за да се предотврати (като се има предвид, че това е пример за играчка и всъщност има неща, които се случват вътре в lock в реалния код)?

.net c# code-contracts
person Philip C    schedule 22.04.2013    source източник
comment
Очевидно Code Contracts не счита инстанцията на o1, която се появява автоматично по време на изпълнение на конструктора, като достатъчно доказателство, гарантиращо o1!=null. Ensures е постусловие и lock предполага, че методът ще бъде извикан от множество нишки.   -  person Robert Harvey    schedule 22.04.2013
comment
@RobertHarvey Но както казах, ако промените this.o1 = new object() в this.o2 = new object(), всичко е наред. Не може да гарантира нищо в този случай, което не може да бъде гарантирано и в оригиналния случай, и все още включва заключване. И Requires трябва да е достатъчно доказателство, че o1 не е нула в началото на метода.   -  person Philip C    schedule 23.04.2013

Отговори (2)


arrow_upward
2
arrow_downward

Ето как статичната проверка третира заключванията и инвариантите:

Ако заключите нещо с формата lock(x.foo) { ... }, статичната проверка счита x.foo за защитна ключалка на x. В края на обхвата на заключване се приема, че други нишки могат да имат достъп до x и да го променят. В резултат на това статичната проверка приема, че всички полета на x удовлетворяват само инварианта на обекта след обхвата на заключване, нищо повече.

Обърнете внимание, че това не разглежда всички вплитания на нишки, а само вплитания в края на обхвата на заключване.

person Manuel Fahndrich    schedule 24.04.2013

arrow_upward
1
arrow_downward

Добавете следния код към вашия клас:

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(o1 != null);
    }

Не мога да ви кажа защо, но в този случай статичният верификатор изглежда счита присвояването на частно поле и липсата на методи, които го модифицират, като достатъчно доказателство, че полето няма да бъде променено. Може ли да е грешка във верификатора? Може би си струва да докладвате във форума за договори за код.

person Stephen J. Anderson    schedule 24.04.2013
comment
Виждам как това ще поправи нещата, но в моя реален клас това всъщност не е инвариант - просто винаги е вярно, преди този метод да бъде извикан, и методът не променя този факт. - person Philip C; 24.04.2013