Introduce Assertion refactoring using Code contracts

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs by offering a number of attributes and helper classes to help formalize any assumptions you make in your code into a contract. A contract can pertain to pre-conditions, post-conditions, assumptions and “object invariants” that enable static contract verification and runtime checking of values.

The Introduce Assertion refactoring recommends making an assumption explicit with an assertion if a section of code is going to make that assumption about the state of the program. You can use code contracts to implement this refactoring in your code. In this post, we’ll see how to refactor your code to add code contracts for assumptions.

[TestMethod]

public void TransferDepositsRequestedAmountInTheAccountFromTheCurrentAccount()

{

    var account = new Account(300);

    var accountToTransfer = new Account();

    account.Transfer(accountToTransfer, 150);

    Assert.AreEqual(account.GetBalance(), 150);

}

public decimal Transfer(Account account, decimal amount)

{

    _accountBalance -= amount;

    account.Deposit(amount);

    return _accountBalance;

}

The code given assumes that the client that calls the transfer method on the current account object passes a valid account object to the transfer method to do the transfer.  

We can prevent the object from being instable by adding assert assumptions as given below.

[TestMethod]

[ExpectedException(typeof(AssertFailedException))]

public void TransferDepositsRequestedAmountInTheAccountFromTheCurrentAccount()

{

    var account = new Account(300);

    var accountToTransfer = default(Account);

    account.Transfer(accountToTransfer, 150);

    Assert.AreEqual(account.GetBalance(), 150);

}

public decimal Transfer(Account account, decimal amount)

{

    Assert.IsNotNull(account);

    _accountBalance -= amount;

    account.Deposit(amount);

    return _accountBalance;

}

Apart from checking that account should not be null, we need to make further assumptions or verifications on the code before we do the actual transfer. We need to make sure that the account has the required balance before transferring the amount to the other account. Also after the transfer the account should have a minimum balance according to the requirements.

Let’s see how code contracts can be used to add the required assumptions and verifications on the code.

[TestMethod, ExpectContractFailure]

public void TransferDepositsRequestedAmountInTheAccountFromTheCurrentAccount()

{

    var account = new Account(300);

    var accountToTransfer = new Account();

    account.Transfer(accountToTransfer, 300);

    Assert.AreEqual(account.GetBalance(), 50);

}

public decimal Transfer(Account account, decimal amount)

{

    Contract.Requires(account != null);

    Contract.Ensures(Contract.Result<decimal>() >= _minimumBalance);

    Contract.Assume(amount < _accountBalance);

    _accountBalance -= amount;

    account.Deposit(amount);

    return _accountBalance;

}

The ExpectContractFailure attribute is a custom attribute created to assert the ContactFailed exception.

public class ExpectContractFailureAttribute : ExpectedExceptionBaseAttribute

{

    const string ContractExceptionName = "System.Diagnostics.Contracts.__ContractsRuntime+ContractException";

    protected override void Verify(Exception exception)

    {

        if (exception.GetType().FullName != ContractExceptionName)

        {

            RethrowIfAssertException(exception);

            throw new ArgumentException("Exception {0} as found instead of contract exception.",

                                        exception.GetType().FullName);

        }

    }

}