The proof of the first two points is pretty straight forward. Because the transaction is assigned prior to calling the service function, we know the service function has a transaction. And because the transaction is created in a using statement, we know that it will be disposed.

The third point is harder to prove. If two threads call GetOrder on the same object, they will both try to assign a transaction to the same OrderServiceProvider. We have to prove that this won't happen. For that, we look at the Castle configuration:

<component
    id="...OrderService"
    service="...OrderService, ..."
    type="...OrderService, ..."
    lifestyle="transient”>
        <parameters>
            <orderRepository>
                ${...OrderRepository}
            </orderRepository>
        </parameters>
</component>

Because the OrderService is declared to be transient, we are guaranteed to get a new instance each time the component is resolved. Each web request resolves the service, so we know that each web request gets a unique object. The request is thread safe. Q.E.D.

Perils of imperative proofs
While these proofs are correct, there is a significant problem. We proved correctness based on the code that calls OrderService, not based on OrderService itself. In fact, there is nothing about the OrderService API that compels the caller to use it correctly.

For example, the service requires that we set the BusinessTransactionContext property before we call a method. If we forget one little assignment statement, then the service does not have a transaction. This problem can be caught no earlier than integration testing.

If, on the other hand, we forget to create our transaction in a using statement, we have a more subtle problem. We may see that database connections leak over time. Or we may see blocking because failed transactions remain open instead of being rolled back. This problem won't be caught in integration testing, and may be very difficult to diagnose when it finally is identified.

And what if we forget to configure our components to be transient? The only time this causes a measurable problem is when we have concurrency greater than 1. This doesn't happen during a typical integration test. Nor does this usually happen during manual testing. The first time a web application sees concurrency is usually during stress testing, or maybe even production.

This lead into a discussion of prerequisites. There are ways that we can rewrite the OrderService API so that it cannot be used incorrectly. Some examples are to require a parameter and to use the constructor. We'll apply these techniques to the OrderService in the next post.