The constructor has a very powerful contract, and one that the compiler proves. The constructor is called once and only once.

We can use this promise to prove some very useful things. We can prove that required properties are set. We can prove that A happens before B (as we can with other prerequisite techniques). But more strongly, we can prove that A does not happen after B.

Required properties
A constructor has to be called. There is no other way to get an instance of an object. If there are any required properties, they should be constructor parameters. Otherwise, there is no way to prove that they've been set.

class ReportRequest
{
    // Required parameters.
    private User _requestedBy;
    private Company _requestedFor;

    // Optional parameters.
    private DateTime? _fromDate;
    private DateTime? _toDate;

    public ReportRequest(User requestedBy, Company requestedFor)
    {
        _requestedBy = requestedBy;
        _requestedFor = requestedFor;
    }

    public User RequestedBy
    {
        get { return _requestedBy; }
    }

    public Company RequestedFor
    {
        get { return _requestedFor; }
    }

    public DateTime? FromDate
    {
        get { return _fromDate; }
        set { _fromDate = value; }
    }

    public DateTime? ToDate
    {
        get { return _toDate; }
        set { _toDate = value; }
    }
}

We can prove that the user requesting the report and the company for which the report is requested are specified. The filter parameters are optional.

Immutable properties
Once a constructor is called, it cannot be called again. This is an extremely powerful contract, and can be used to prove that properties can't change. In the above example, the RequestedBy and RequestedFor properties are immutable. They can only be set by the constructor, which can only be called once.

Immutability is an example of the statement A does not happen after B. A) the property changes. B) the property is set. The property does not change after it is set.

There are other statements of this form that the constructor can prove. For example, a connection string cannot change after a database connection has been established. Here's a snippet of the ADO.NET SqlConnection class:

public class SqlConnection
{
    public SqlConnection();
    public SqlConnection(string connectionString);
    public string ConnectionString { get; set; }
}

Do you see the problem? You cannot prove that the connection string does not change. This class has guard code that throws an exception if you do so. It would be a simple change to make this contract provable:

public class SqlConnection
{
    public SqlConnection(string connectionString);
    public string ConnectionString { get; }
}

Don't waste the constructor
Using a constructor to prove a contract is a powerful capability. It is weakened when the constructor is used for other things.

public class User
{
    private string _userId;
    private string _firstName;
    private string _lastName;

    public User(string userId) :
        this(userId, string.Empty, string.Empty)
    {
    }

    public User(string userId, string firstName, string lastName)
    {
        _userId = userId;
        _firstName = firstName;
        _lastName = lastName;
    }

    public string UserId
    {
        get { return _userId; }
    }

    public string FirstName
    {
        get { return _firstName; }
        set { _firstName = value; }
    }

    public string LastName
    {
        get { return _lastName; }
        set { _lastName = value; }
    }
}

This class has a weak constructor. The name of a user can change, but the ID cannot. An overloaded constructor initializing the name is provided for convenience. But this convenience comes at a price. It is more difficult to see that the user ID is required and immutable. It's still provable, but that information is not called out.

Don't overload the constructor. Don't use it for convenience. Don't initialize mutable properties. When a constructor is used only to set required and immutable properties, the intent is clear, and the proof is easy.

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.

When I say "closure", I'm talking about two things. First, there's the language feature. Second, there's the concept. Either way, it is fundamental to proving software.

Language feature
As a language feature, closure is the ability to bring variables into scope and encapsulate them within a function. Different languages support this feature in different ways. In C#, it is supported in lambdas and anonymous delegates.

public Order GetOrder(string orderId)
{
    return GetOrderRepository()
        .GetSatisfying(o => o.OrderId == orderId)
        .Query()
        .FirstOrDefault();
}

The parameter orderId is available within the lambda, even though the lambda executes outside of the scope of this method.

As of Java 6, closure is supported only by anonymous inner classes. It is slated for becoming a first-class language feature in Java 7.

public Order getOrder(final string orderId) {
    return Query
        .from(getOrders())
        .where(new Predicate<Order>() {
            public boolean where(Order row) {
                return row.getOrderId() == orderId;
            }
        })
        .selectOne();
}

Again, the orderId parameter is available within the anonymous inner class. It will be set to the the correct value even though Predicate.where() is called by code not located in the method. In Java, the variables to be enclosed must be marked as "final" to ensure that they are not changed after the closure is created.

Factory methods
As a concept, closure can be used in several places. It doesn't take an explicit language feature to take advantage of the concept. In fact, the Factory Method pattern is often used to perform closure.

A factory method constructs an object, but hides its class. In doing so, it usually takes parameters that are injected into the new object. These parameters obey the laws of closure.

public IOrderService
    CreateOrderService(
        ITransaction transaction)
{
    return new
        OrderService(
            transaction,
            _accountsServiceProvider,
            _catalogServiceProvider);
}

The transaction parameter is enclosed within the object. An object, just like a lambda, is a packet of behavior that can be executed later. The value of transaction is already set at the time that the behavior is executed.

Constructors
Notice that there are two other parameters passed into the OrderService. These two are set in the constructor of the factory itself.

private IServiceProvider<IAccountsService> _accountsServiceProvider;
private IServiceProvider<ICatalogService> _catalogServiceProvider;

public OrderServiceFactory(
    IServiceProvider<IAccountsService> accountsServiceProvider,
    IServiceProvider<ICatalogService> catalogServiceProvider)
{
    _accountsServiceProvider = accountsServiceProvider;
    _catalogServiceProvider = catalogServiceProvider;
}

The factory encloses some parameters and forwards them on to all of the objects it creates. In this way, closure can be nested.

Just like the "final" parameter in the Java example, we don't want these values changing. For the same reason that Java requires the "final" keyword for closure, fields initialized by the constructor should be considered immutable.

Closure is a useful mechanism for writing provable software. Whether we use it as a language feature or simply as a pattern, it allows us to bring values into a function or object. We can then prove interesting things about those values, as we will see in coming posts.