Статический контракт недоказан, потому что ссылка передается другому методу (который только читает)

Question

У кого-то еще были проблемы с контрактами.У меня есть следующее:

public void doSomeThing(Stack stack)
{
    Contract.Requires(stack != null);

    stack.Push("$");
    Contract.Assert(stack.Count > 0); //redundant check
    _Look(stack);
    Contract.Assert(stack.Count > 0); //this contract fails static analysis, because analyser does not know that _Look does not write to stack.
    stack.Pop();
}

private void _Look(Stack stack)
{
    //do nothing
}

Второе утверждение не доказано, потому что вызов _Look может (но не изменяет) содержимое стека.Есть ли способ сказать, что _Look не меняет стек?Или есть какой-то другой способ заставить это работать?

Обратите внимание, что эти контракты проходят динамически, просто второй не может быть доказан статически.

Answer 1

Таким образом, создается впечатление, что вы используете контракты для проверки правильности работы вашего метода _Look.Я считаю, что правильный способ сделать это - перенести предварительные и последующие проверки в метод _Look.Для того, чтобы быть с вашим первым утверждением, нет необходимости, если вы не доверяете стеку, который находится вне вашего контроля.В свете этого я бы сделал следующее:

public void doSomeThing(Stack stack)
{
    Contract.Requires(stack != null);

    stack.Push("$");
    _Look(stack);
    stack.Pop();
}

private void _Look(Stack stack)
{
    Contract.Requires(stack != null);
    Contract.Requires(stack.Count > 0);

    //do something here

    Contract.Assert(stack.Count > 0);     
}

Контракты предназначены для предварительной и последующей проверки, а не утверждения в середине кода.

Answer 2

Этот ответ основан на идее чтения ответа Крейга Уилсона.

public void doSomeThing(Stack stack)
{
    Contract.Requires(stack != null);

    stack.Push("$");
    Contract.Assert(stack.Count > 0); //redundant check
    _Look(stack);
    Contract.Assert(stack.Count > 0); //this contract fails static analysis, because analyser does not know that _Look does not write to stack.
    stack.Pop();
}

private void _Look(Stack stack)
{
    Contract.Ensures(stack.Count == Contract.OldValue(stack.Count));
}

Answer 3

Поскольку Code Contracts ничего не знает о том, что делает метод _Look, он не может знать, что Count останется прежним.Вы должны явно сказать это так:

private void _Look(Stack stack)
{
    Contract.Ensures(stack.Count == Contract.OldValue(stack.Count));

    //do nothing
}

Answer 4

Я не знаю, что здесь происходит.Второе утверждение должно пройти.Если вы ничего не высовываете.Это должно остаться там.Единственное, что здесь есть, это толкать, выдвигать и утверждать.