CODEWITHSUNDEEP
.netcode-contracts
WebMonster
WebMonster

Reputation: 3031

How to hint static checker to understand simple arithmetics?

I am working on an object that encapsulates a bitmap as an array of pixels. The array is one dimensional, and I store the width of the image in a readonly field. I also added a property that calculates the height based the pixel array length and the width. I have the following invariants regarding the height:

The code of the height property:

public int Height
{
    [Pure]
    get
    {
        Contract.Requires(Data != null);
        Contract.Requires(Width > 0);
        Contract.Requires(Data.Length > 0);

        Contract.Ensures(Contract.Result<int>() > 0);
        Contract.EndContractBlock();
        Contract.Assume(Data.Length > Width);

        return Data.Length / Width;
    }
}

But I can't get the static checker to prove the ensure. The problem might be (as of my understanding), that there is no requirement that Data.Length % Width == 0, so because of the integer division Data.Length / Width could be zero; hence I added the assumption with no luck. I am not sure how to hint the static checker to accept my ensure.

Upvotes: 1

Views: 57

Answers (1)

Mightymuke
Mightymuke

Reputation: 5144

I wrote a simple little test, and it seemed to pass

The test object class:

public class Class1
{
    public int Width { get; set; }
    public byte[] Data { get; set; }

    public int Height
    {
        [Pure]
        get
        {
            Contract.Requires(Data != null);
            Contract.Requires(Width > 0);
            Contract.Requires(Data.Length > 0);

            Contract.Ensures(Contract.Result<int>() > 1);
            //Contract.Assume(Data.Length > Width);

            return Data.Length / Width;
        }
    }
}

The unit test:

[TestFixture]
public class Tests
{
    [Test]
    public void Class1_ContractEnsures_IsEnforced()
    {
        var item = new Class1 { Width = 1, Data = new byte[1] };
        var h = item.Height;
    }
}

Note that if I re-enable the Assume constraint, then this will fire first (and fail) so the Ensures wont be tested. The Unit test was included to create a call to Height. Without this, code contracts seemed to detect that Height wasn't used so wouldn't apply the ensure constraint. Also the error message I received was CodeContracts: requires is false which may be a little misleading.

I'm using Code Contracts 1.4.50327.0 if that helps?

Upvotes: 1

Related Questions