2

私は Code Contracts で遊んでいますが、これまで見てきたものが本当に気に入っています。彼らは、自分の仮定を評価して明示的に宣言するように勧めてくれます。これは、コントラクトを追加するコードで考慮していなかったいくつかのコーナー ケースを特定するのにすでに役立ちました。現在、私はより洗練された不変条件を適用しようとして遊んでいます。現在、証明に失敗しているケースが 1 つあります。単純に 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 に答える