Code Contracts Static Analysis: Prover Limitations?

Question

I've been playing with Code Contracts and I really like what I've seen so far. They encourage me to evaluate and explicitly declare my assumptions, which has already helped me to identify a few corner cases I hadn't considered in the code to which I'm adding contracts. Right now I'm playing with trying to enforce more sophisticated invariants. I have one case that currently fails proving and I'm curious if there is a way I can fix this besides simply adding Contract.Assume calls. Here is the class in question, stripped down for ease of reading:

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);
    }
}

I'm interested in how I can structure the Contract calls in ReserveSpace so that the class invariants are provable. In particular, it complains about (Length <= Buffer.Length) and (CurrentByte <= Length). It's reasonable to me that it can't see that (Length <= Buffer.Length) is satisfied, since it's creating a new buffer and reassigning the reference. Is my only option to add an Assume that the invariants are satisfied?

Answer 1

After fighting with this for a while, I came up with this provable solution (constructor is a dummy to allow for isolated testing):

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);
    }
}

The main thing I noticed is that placing invariants on properties gets messy, but seems to solve more easily with invariants on fields. It was also important to place appropriate contractual obligations in the property accessors. I'll have to keep experimenting and see what works and what doesn't. It's an interesting system, but I'd definitely like to know more if anybody has a good 'cheat sheet' on how the prover works.