Proving prerequisites

Every piece of code is a theorem. It is a sequence of logical conclusions, each based on the one before, leading up to desired behavior. To validate that behavior, you need to prove the theorem. Even though most compilers don't prove those theorems for you, they can still provide some assistance.

We often have to call methods in a certain order. One method is a prerequisite, the other its successor. For example, we need to validate a shopping cart before we check out. Typically, this is hard to prove.

public class ShoppingCart
{
    /// <summary>
    /// Validate the shopping cart. Throws
    /// ShoppingCartException if there is a problem.
    /// </summary>
    public void Validate() { }

    /// <summary>
    /// Checkout and provide payment for a shopping
    /// cart. Requires that Validate() is called first.
    /// </summary>
    /// <param name="paymentMethod">Method used to pay
    /// for the items in the car.</param>
    public void Checkout(IPaymentMethod paymentMethod) { }
}

The contract is clear, but how do we prove that the caller is following the rules? One way is to keep an internal flag. Set it in Validate(), and check it in Checkout(). If the flag is false, throw an exception.

While this technique works, it is not ideal. It is really no different from a guard clause. It's just a different form of defensive programming. Besides, exceptions are for problems that occur even in well-written software. Calling Checkout() without calling Validate() is a defect, and should never happen at all.

Return from a prerequisite
If we change the interface, we can prove the contract at compile time. It won't need to be verified at run time. One way to do this is to put the successor method into the return of its prerequisite.

public interface IValidatedShoppingCart
{
    /// <summary>
    /// Checkout and provide payment for a shopping
    /// cart.
    /// </summary>
    /// <param name="paymentMethod">Method used to pay
    /// for the items in the car.</param>
    void Checkout(IPaymentMethod paymentMethod);
}

public class ShoppingCart
{
    /// <summary>
    /// Validate the shopping cart. Throws
    /// ShoppingCartException if there is a problem.
    /// </summary>
    public IValidatedShoppingCart Validate() { }
}

The compile-time contract is strong enough that it could be removed from the comment. It's obvious to the caller that they have to call Validate() first.

Pass a parameter to the successor
Another way to prove the contract as compile time is to pass the prerequisite as a parameter to the successor. We could, for example, prove that the caller needs to get a credit card approved before using it to make a purchase. Here's the hard way.

public class CreditCard : IPaymentMethod
{
    /// <summary>
    /// Create a credit card for a customer.
    /// </summary>
    /// <param name="customerInfo">Information
    /// about the card holder.</param>
    public CreditCard(CustomerInfo customerInfo) { }

    /// <summary>
    /// Request approval for a credit card. If
    /// approved, return the payment. If not,
    /// CreditCardException is thrown.
    /// </summary>
    public void Approve() { }
}

We could set a flag when Approve() is called, and check it when the IPaymentMethod is used. But again, it is defensive. There is a better way.

public class CustomerInfo
{
    /// <summary>
    /// Request approval for a credit card. If
    /// approved, return the payment. If not,
    /// CreditCardException is thrown.
    /// </summary>
    /// <returns>Payment that can be used to
    /// purchase items.</returns>
    IPaymentMethod Approve() { }
}

We've taken away the ability to create a CreditCard, and hidden it in Approve(). The result of Approve() is a parameter to Checkout(). We've proven that the caller must call the prerequisite before the successor.

A simple rearrangement of interfaces can turn a difficult-to-enforce API into one that the compiler can prove. Just recognize which methods are prerequisites of others, and use their returns to call the successors.

Leave a Reply

You must be logged in to post a comment.