2

我一直在玩 Code Contracts，我真的很喜欢我目前所看到的。他们鼓励我评估并明确声明我的假设，这已经帮助我确定了一些我在添加合同的代码中没有考虑过的极端情况。现在我正在尝试强制执行更复杂的不变量。我有一个案例目前无法证明，我很好奇除了简单地添加 Contract.Assume 调用之外是否还有其他方法可以解决这个问题。这是有问题的课程，为了便于阅读而被剥离：

public abstract class MemoryEncoder
{
    private const int CapacityDelta = 16;

    private int _currentByte;

    /// <summary>
    ///   The current byte index in the encoding stream.
    ///   This should not need to be modified, under typical usage,
    ///   but can be used to randomly access the encoding region.
    /// </summary>
    public int CurrentByte
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() >= 0);
            Contract.Ensures(Contract.Result<int>() <= Length);
            return _currentByte;
        }
        set
        {
            Contract.Requires(value >= 0);
            Contract.Requires(value <= Length);
            _currentByte = value;
        }
    }

    /// <summary>
    ///   Current number of bytes encoded in the buffer.
    ///   This may be less than the size of the buffer (capacity).
    /// </summary>
    public int Length { get; private set; }

    /// <summary>
    /// The raw buffer encapsulated by the encoder.
    /// </summary>
    protected internal Byte[] Buffer { get; private set; }

    /// <summary>
    /// Reserve space in the encoder buffer for the specified number of new bytes
    /// </summary>
    /// <param name="bytesRequired">The number of bytes required</param>
    protected void ReserveSpace(int bytesRequired)
    {
        Contract.Requires(bytesRequired > 0);
        Contract.Ensures((Length - CurrentByte) >= bytesRequired);

        //Check if these bytes would overflow the current buffer););
        if ((CurrentByte + bytesRequired) > Buffer.Length)
        {
            //Create a new buffer with at least enough space for the additional bytes required
            var newBuffer = new Byte[Buffer.Length + Math.Max(bytesRequired, CapacityDelta)];

            //Copy the contents of the previous buffer and replace the original buffer reference
            Buffer.CopyTo(newBuffer, 0);
            Buffer = newBuffer;
        }

        //Check if the total length of written bytes has increased
        if ((CurrentByte + bytesRequired) > Length)
        {
            Length = CurrentByte + bytesRequired;
        }
    }

    [ContractInvariantMethod]
    private void GlobalRules()
    {
        Contract.Invariant(Buffer != null);
        Contract.Invariant(Length <= Buffer.Length);
        Contract.Invariant(CurrentByte >= 0);
        Contract.Invariant(CurrentByte <= Length);
    }
}

我对如何在 ReserveSpace 中构造 Contract 调用感兴趣，以便类不变量是可证明的。特别是，它抱怨 (Length <= Buffer.Length) 和 (CurrentByte <= Length)。对我来说，它看不到满足 (Length <= Buffer.Length) 是合理的，因为它正在创建一个新缓冲区并重新分配引用。我唯一的选择是添加一个假设满足不变量吗？

4

1 回答 1

3

在与这个问题斗争了一段时间之后，我想出了这个可证明的解决方案（构造函数是一个允许隔离测试的假人）：

public abstract class MemoryEncoder
{
    private const int CapacityDelta = 16;

    private byte[] _buffer;
    private int _currentByte;
    private int _length;

    protected MemoryEncoder()
    {
        Buffer = new byte[500];
        Length = 0;
        CurrentByte = 0;
    }

    /// <summary>
    ///   The current byte index in the encoding stream.
    ///   This should not need to be modified, under typical usage,
    ///   but can be used to randomly access the encoding region.
    /// </summary>
    public int CurrentByte
    {
        get
        {
            return _currentByte;
        }
        set
        {
            Contract.Requires(value >= 0);
            Contract.Requires(value <= Length);
            _currentByte = value;
        }
    }


    /// <summary>
    ///   Current number of bytes encoded in the buffer.
    ///   This may be less than the size of the buffer (capacity).
    /// </summary>
    public int Length
    {
        get { return _length; }
        private set
        {
            Contract.Requires(value >= 0);
            Contract.Requires(value <= _buffer.Length);
            Contract.Requires(value >= CurrentByte);
            Contract.Ensures(_length <= _buffer.Length);
            _length = value;
        }
    }

    /// <summary>
    /// The raw buffer encapsulated by the encoder.
    /// </summary>
    protected internal Byte[] Buffer
    {
        get { return _buffer; }
        private set
        {
            Contract.Requires(value != null);
            Contract.Requires(value.Length >= _length);
            _buffer = value;
        }
    }

    /// <summary>
    /// Reserve space in the encoder buffer for the specified number of new bytes
    /// </summary>
    /// <param name="bytesRequired">The number of bytes required</param>
    protected void ReserveSpace(int bytesRequired)
    {
        Contract.Requires(bytesRequired > 0);
        Contract.Ensures((Length - CurrentByte) >= bytesRequired);

        //Check if these bytes would overflow the current buffer););
        if ((CurrentByte + bytesRequired) > Buffer.Length)
        {
            //Create a new buffer with at least enough space for the additional bytes required
            var newBuffer = new Byte[Buffer.Length + Math.Max(bytesRequired, CapacityDelta)];

            //Copy the contents of the previous buffer and replace the original buffer reference
            Buffer.CopyTo(newBuffer, 0);
            Buffer = newBuffer;
        }

        //Check if the total length of written bytes has increased
        if ((CurrentByte + bytesRequired) > Length)
        {
            Contract.Assume(CurrentByte + bytesRequired <= _buffer.Length);
            Length = CurrentByte + bytesRequired;
        }
    }

    [ContractInvariantMethod]
    private void GlobalRules()
    {
        Contract.Invariant(_buffer != null);
        Contract.Invariant(_length <= _buffer.Length);
        Contract.Invariant(_currentByte >= 0);
        Contract.Invariant(_currentByte <= _length);
    }
}

我注意到的主要事情是在属性上放置不变量会变得混乱，但似乎在字段上使用不变量更容易解决。对财产访问者规定适当的合同义务也很重要。我将不得不继续试验，看看哪些有效，哪些无效。这是一个有趣的系统，但如果有人有关于证明者如何工作的好的“备忘单”，我肯定想知道更多。

于 2010-06-19T00:25:05.000 回答